OAI/NumberTheory/Ostmann/ZeroDensity/RealCharacterComplexification.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Real characters inside the actual complex-character zero development

  1. theorem OAI.Ostmann.PrimitiveRealCharacter.complex_factorsThrough_iff line 12
  2. theorem OAI.Ostmann.PrimitiveRealCharacter.complex_conductor line 28
  3. def OAI.Ostmann.PrimitiveRealCharacter.asComplex line 36

    Source documentation

    The coercion to complex values preserves the actual conductor and character.

    noncomputable def PrimitiveRealCharacter.asComplex (χ : PrimitiveRealCharacter) :
    PrimitiveComplexCharacter where
…

    Mentions: OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.PrimitiveComplexCharacter

  4. theorem OAI.Ostmann.PrimitiveRealCharacter.asComplex_L line 46
  5. def OAI.Ostmann.realCharacterActualZeros line 49