OAI/NumberTheory/Ostmann/Characters/CharacterRepeatedTuplesPrior.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.characterTuplePrior line 15
  2. def OAI.Ostmann.Characters.characterTupleProduct line 19
  3. def OAI.Ostmann.Characters.characterTuplePeriod line 21
  4. lemma OAI.Ostmann.Characters.characterTupleProduct_pos line 24
  5. lemma OAI.Ostmann.Characters.characterTuplePeriod_pos line 27
  6. lemma OAI.Ostmann.Characters.characterTuplePrior_mass_eq_zero line 31
  7. lemma OAI.Ostmann.Characters.characterTuplePrior_mass_le line 39
  8. lemma OAI.Ostmann.Characters.characterTuple_reciprocal_period line 55
  9. theorem OAI.Ostmann.Characters.characterTuple_supported_reciprocal_sum_le line 67