OAI/NumberTheory/Ostmann/Arithmetic/HistoryResidueRegular.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryResidueRegular.Regular line 9
2. theorem OAI.Ostmann.Arithmetic.HistoryResidueRegular.intCast_ne_zero_of_natAbs_lt line 17
3. theorem OAI.Ostmann.Arithmetic.HistoryResidueRegular.supported_regular line 24
4. theorem OAI.Ostmann.Arithmetic.HistoryResidueRegular.frequency_ne_zero line 46
5. theorem OAI.Ostmann.Arithmetic.HistoryResidueRegular.value_ne_zero line 49
6. theorem OAI.Ostmann.Arithmetic.HistoryResidueRegular.left_regular line 54
7. theorem OAI.Ostmann.Arithmetic.HistoryResidueRegular.right_regular line 58