lean_workbook_plus_23365
ProvedIf there exists such that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23365 {a b : ℕ} (hab : Nat.Coprime a b) : ∃ n, a*n ≡ 1 [ZMOD b] := by sorrySource
If there exists such that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_23365 {a b : ℕ} (hab : Nat.Coprime a b) : ∃ n, a*n ≡ 1 [ZMOD b] := by sorry