mathlib documentation

field_theory.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 finite_field.trace_to_zmod_nondegenerate (F : Type u_1) [field F] [fintype F] {a : F} (ha : a 0) :
∃ (b : F), (algebra.trace (zmod (ring_char F)) F) (a * b) 0

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