Theorem: frobeniusMorphism_injective (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
⊢ Injective ↑(frobeniusMorphism p K)
Tactic:
have : ∀ x : K, x ^ p = 0 → x = 0 := by exact?
State after:
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
this : ∀ (x : K), x ^ p = 0 → x = 0
⊢ Injective ↑(frobeniusMorphism p K)

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
this : ∀ (x : K), x ^ p = 0 → x = 0
⊢ Injective ↑(frobeniusMorphism p K)
Tactic:
sorry
State after:
no goals

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
⊢ ∀ (x : K), x ^ p = 0 → x = 0
Tactic:
exact?
State after:
no goals