OAI/NumberTheory/Ostmann/Quadratic/QuadraticCharacterReal.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Quadratic complex characters as real primitive characters

  1. theorem OAI.Ostmann.quadratic_character_im_zero line 11
  2. def OAI.Ostmann.realPartCharacter line 20
  3. theorem OAI.Ostmann.realPartCharacter_complexification line 29
  4. theorem OAI.Ostmann.complexification_conductor line 37
  5. def OAI.Ostmann.PrimitiveComplexCharacter.asReal line 57
  6. theorem OAI.Ostmann.PrimitiveComplexCharacter.asReal_asComplex line 73