OAI/NumberTheory/Ostmann/Characters/CharacterFaithfulEnumeration.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A faithful enumeration of all actual zeros with their multiplicities

  1. theorem OAI.Ostmann.characterZeroCopy_countable line 14
  2. theorem OAI.Ostmann.characterZeroCopy_infinite line 24
  3. def OAI.Ostmann.faithfulCharacterZeroEquiv line 37

    Source documentation

    No dummy zeros, repetitions, or omitted multiplicity labels occur.

    noncomputable def faithfulCharacterZeroEquiv (χ : PrimitiveComplexCharacter) :
    ℕ ≃ CharacterZeroCopy χ := by
…

    Mentions: OAI.Ostmann.PrimitiveComplexCharacter, OAI.Ostmann.CharacterZeroCopy

  4. def OAI.Ostmann.actualCharacterZeros line 43
  5. theorem OAI.Ostmann.actualCharacterZeros_respectsMultiplicity line 46