case a
K : Type ?u.1003397
R : Type ?u.1003400
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ ↑(frobenius (ZMod p) p) a = ↑(RingHom.id (ZMod p)) a
K : Type ?u.1003397
R : Type ?u.1003400
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ frobenius (ZMod p) p = RingHom.id (ZMod p)
ext a
no goals
case a
K : Type ?u.1003397
R : Type ?u.1003400
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ZMod p
⊢ ↑(frobenius (ZMod p) p) a = ↑(RingHom.id (ZMod p)) a
rw [frobenius_def, ZMod.pow_card, RingHom.id_apply]