OAI/NumberTheory/Ostmann/Arithmetic/HistoryPairNumerators.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistoryPairNumerators.actual line 12
2. theorem OAI.Ostmann.Arithmetic.HistoryPairNumerators.actual_divisible line 15
3. theorem OAI.Ostmann.Arithmetic.HistoryPairNumerators.actual_linear line 21
4. theorem OAI.Ostmann.Arithmetic.HistoryPairNumerators.integer_linear_cleared line 32
5. theorem OAI.Ostmann.Arithmetic.HistoryPairNumerators.actual_line_zero line 58
6. theorem OAI.Ostmann.Arithmetic.HistoryPairNumerators.frequency_units line 74
7. theorem OAI.Ostmann.Arithmetic.HistoryPairNumerators.actual_power_dvd_iff line 82