Theorem: iterate_frobeniusMorphism (LeanCourse/Lectures/Lecture10.lean)

State before:
R : Type u_1
M : Type u_2
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_3
inst✝¹ : Field K
inst✝ : CharP K p
x : K
n : ℕ
⊢ (↑(frobeniusMorphism p K))^[n] x = x ^ p ^ n
Tactic:
sorry
State after:
no goals