K : Type ?u.1090717
R : Type ?u.1090720
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]
K : Type ?u.1090717
R : Type ?u.1090720
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]
haveI : Fact p.Prime := ⟨hp⟩
no goals
K : Type ?u.1090717
R : Type ?u.1090720
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this✝ : Fact (Nat.Prime p)
this : ¬↑n = 0
⊢ n ^ (p - 1) ≡ 1 [ZMOD ↑p]
simpa [← ZMod.int_cast_eq_int_cast_iff] using ZMod.pow_card_sub_one_eq_one this
K : Type ?u.1090717
R : Type ?u.1090720
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p) n
K : Type ?u.1090717
R : Type ?u.1090720
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ ¬↑n = 0
rw [CharP.int_cast_eq_zero_iff _ p, ← (Nat.prime_iff_prime_int.mp hp).coprime_iff_not_dvd]
no goals
K : Type ?u.1090717
R : Type ?u.1090720
p : ℕ
hp : Nat.Prime p
n : ℤ
hpn : IsCoprime n ↑p
this : Fact (Nat.Prime p)
⊢ IsCoprime (↑p) n
exact hpn.symm