FiniteField.trace_to_zmod_nondegenerate

theorem FiniteField.trace_to_zmod_nondegenerate : ∀ (F : Type u_1) [inst : Field F] [inst_1 : Finite F] [inst_2 : Algebra (ZMod (ringChar F)) F] {a : F}, a ≠ 0 → ∃ b, (Algebra.trace (ZMod (ringChar F)) F) (a * b) ≠ 0

This theorem states that the trace map from a finite field to its prime field is nondegenerate. In other words, for any finite field `F` with a given characteristic, and for any non-zero element `a` in this field, there exists some element `b` such that the trace of `a * b`, as calculated via an algebra structure defined over modulated integers of the field's characteristic and the field itself, is not zero. The "trace" here refers to the trace of an element `s` of an `R`-algebra, which is defined as the trace of `(s * ·)`, considered as an `R`-linear map.

More concisely: For any finite field `F` and non-zero element `a` in `F`, there exists an element `b` in `F` such that the trace of `a` * `b` with respect to the multiplication algebra of `F` over its prime field is non-zero.