case intro
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ↑k * (↑k)⁻¹ = 1
n a✝ p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
h : a ≠ 0
⊢ a * a⁻¹ = 1
obtain ⟨k, rfl⟩ := nat_cast_zmod_surjective a
case intro.h
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ Nat.coprime k p
case intro
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ ↑k * (↑k)⁻¹ = 1
apply coe_mul_inv_eq_one
case intro.h.a
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ Nat.coprime p k
case intro.h
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ Nat.coprime k p
apply Nat.coprime.symm
no goals
case intro.h.a
n a p : ℕ
inst✝ : Fact (Nat.Prime p)
k : ℕ
h : ↑k ≠ 0
⊢ Nat.coprime p k
rwa [Nat.Prime.coprime_iff_not_dvd Fact.out, ← CharP.cast_eq_zero_iff (ZMod p)]