mathlib3 documentation


The trace map for finite fields #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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] [finite F] [algebra (zmod (ring_char F)) 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.