Theorem: frobeniusMorphism_bijective (LeanCourse/Lectures/Lecture10Before.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
inst✝ : Finite K
⊢ Bijective ↑(frobeniusMorphism p K)
Tactic:
sorry
State after:
no goals