[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
haveI : Fact (ringChar F).Prime := ⟨CharP.char_is_prime F _⟩
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
have htr := traceForm_nondegenerate (ZMod (ringChar F)) F a
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), BilinForm.bilin (Algebra.traceForm (ZMod (ringChar F)) F) a n = 0) → a = 0
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
simp_rw [Algebra.traceForm_apply] at htr 
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), ↑(Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
⊢ ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0
[PROOFSTEP]
by_contra' hf
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Finite F
inst✝ : Algebra (ZMod (ringChar F)) F
a : F
ha : a ≠ 0
this : Fact (Nat.Prime (ringChar F))
htr : (∀ (n : F), ↑(Algebra.trace (ZMod (ringChar F)) F) (a * n) = 0) → a = 0
hf : ∀ (b : F), ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) = 0
⊢ False
[PROOFSTEP]
exact ha (htr hf)
