n x : ℕ
h : Nat.gcd (x % n) n = 1
⊢ ↑x * (↑x)⁻¹ = 1
n x : ℕ
h : Nat.coprime x n
⊢ ↑x * (↑x)⁻¹ = 1
rw [Nat.coprime, Nat.gcd_comm, Nat.gcd_rec] at h
no goals
n x : ℕ
h : Nat.gcd (x % n) n = 1
⊢ ↑x * (↑x)⁻¹ = 1
rw [mul_inv_eq_gcd, val_nat_cast, h, Nat.cast_one]