K : Type ?u.1001241
R : Type ?u.1001244
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
K : Type ?u.1001241
R : Type ?u.1001244
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
⊢ x ^ p = x
have h := FiniteField.pow_card x
no goals
K : Type ?u.1001241
R : Type ?u.1001244
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ZMod p
h : x ^ Fintype.card (ZMod p) = x
⊢ x ^ p = x
rwa [ZMod.card p] at h