K : Type ?u.1088147
R : Type ?u.1088150
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : ↑(expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ ↑(expand (ZMod p) p) f = f ^ p
K : Type ?u.1088147
R : Type ?u.1088150
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
⊢ ↑(expand (ZMod p) p) f = f ^ p
have h := FiniteField.expand_card f
no goals
K : Type ?u.1088147
R : Type ?u.1088150
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : (ZMod p)[X]
h : ↑(expand (ZMod p) (Fintype.card (ZMod p))) f = f ^ Fintype.card (ZMod p)
⊢ ↑(expand (ZMod p) p) f = f ^ p
rwa [ZMod.card p] at h