OAI/NumberTheory/Ostmann/Characters/HistoryFrequencyLabelsModulus.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.HistoryFrequencyLabels.labels line 9
  2. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.root_mem_labels line 14
  3. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.mem_labels_range line 18
  4. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.rangeSupported_iff_labels line 34
  5. def OAI.Ostmann.Characters.HistoryFrequencyLabels.modulus line 50
  6. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.modulus_zero line 53
  7. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.modulus_succ line 56
  8. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.frequency_dvd_modulus line 61
  9. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.root_dvd_modulus line 66
  10. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.left_dvd_modulus line 69
  11. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.right_dvd_modulus line 74
  12. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.modulus_pos line 79
  13. theorem OAI.Ostmann.Characters.HistoryFrequencyLabels.modulusNeZero line 88