mathlib3 documentation

field_theory.finite.trace

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

source
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.