Theorems · Inductive type · number theory

AddChar.PrimitiveAddChar

(R : Type u) → [CommRing R] → (R' : Type v) → [Field R'] → Type (max u v)

Definition for a primitive additive character on a finite ring R into a cyclotomic extension of a field R'. It records which cyclotomic extension it is, the character, and the fact that the character is primitive.

Defined in

Mathlib.NumberTheory.LegendreSymbol.AddCharacter

Cited by

7 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

CommRingField