Theorems · Definition · number theory

AddChar.FiniteField.primitiveChar

(F : Type u_1) →
  (F' : Type u_2) →
    [inst : Field F] → [Finite F] → [inst_2 : Field F'] → ringChar F' ≠ ringChar F → AddChar.PrimitiveAddChar F F'

There is a primitive additive character on the finite field F if the characteristic of the target is different from that of F. We obtain it as the composition of the trace from F to ZMod p with a primitive additive character on ZMod p, where p is the characteristic of F.

Defined in

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Cited by

3 results in Mathlib

Foundations

Depth 220 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFiniteField