Documentation

Mathlib.FieldTheory.Finite.Trace

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.