OAI/NumberTheory/Ostmann/Characters/PrimitiveCharacterReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Reduction to the actual primitive character, without multiplicities

At a fixed ambient modulus, passage to primitive characters is injective. Thus grouping the sparse expansion introduces no coefficient multiplicity.

  1. theorem OAI.Ostmann.primitiveCharacter_nontrivial line 13
  2. def OAI.Ostmann.primitiveCharacterReduction line 20
  3. def OAI.Ostmann.liftPrimitiveCharacter line 29
  4. theorem OAI.Ostmann.lift_primitiveCharacterReduction line 35
  5. theorem OAI.Ostmann.primitiveCharacterReduction_injective line 44
  6. theorem OAI.Ostmann.primitiveCharacterReduction_modulus line 50
  7. theorem OAI.Ostmann.primitiveCharacterReduction_modulus_le line 58