The trace map for finite fields

We state the fact that the trace map from a finite field of characteristic p to ZMod p is nondegenerate.

Tags

finite field, trace

theorem FiniteField.trace_to_zmod_nondegenerate (F : Type u_1) [Field F] [Finite F] [Algebra (ZMod (ringChar F)) F] {a : F} (ha : a ≠ 0) : ∃ b, ↑(Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

The trace map from a finite field to its prime field is nongedenerate.