OAI/NumberTheory/Ostmann/Arithmetic/HistoryProductWindowsNormalize.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.inheritedCenter_nominal_error line 13
2. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.removedCenter_nominal_error line 31
3. def OAI.Ostmann.Arithmetic.HistoryProductWindows.nominalInheritedWidth line 37
4. def OAI.Ostmann.Arithmetic.HistoryProductWindows.nominalRemovedWidth line 38
5. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.inherited_window_normalize line 40
6. theorem OAI.Ostmann.Arithmetic.HistoryProductWindows.removed_window_normalize line 62