no goals
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
⊢ (↑(frobenius R p)^[n]) x = x ^ p ^ n
induction n with
| zero => simp
| succ n n_ih =>
    rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]
no goals
case zero
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
⊢ (↑(frobenius R p)^[Nat.zero]) x = x ^ p ^ Nat.zero
simp
no goals
case succ
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type v
inst✝³ : CommSemiring S
f : R →* S
g : R →+* S
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : CharP R p
inst✝ : CharP S p
x y : R
n : ℕ
n_ih : (↑(frobenius R p)^[n]) x = x ^ p ^ n
⊢ (↑(frobenius R p)^[Nat.succ n]) x = x ^ p ^ Nat.succ n
rw [Function.iterate_succ', pow_succ', pow_mul, Function.comp_apply, frobenius_def, n_ih]