haveI : Fact p.Prime := ⟨hp⟩
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
⊢ n ^ p ≡ n [ZMOD ↑p]
R : Type u
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : ℕ
hp : Nat.Prime p
n : ℤ
this : Fact (Nat.Prime p)
⊢ n ^ p ≡ n [ZMOD ↑p]