OAI/NumberTheory/Ostmann/Arithmetic/HistoryProductWindows.lean
7 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Ostmann.Arithmetic.HistoryProductWindows.inheritedCenterline 13 - def
OAI.Ostmann.Arithmetic.HistoryProductWindows.removedCenterline 16 - def
OAI.Ostmann.Arithmetic.HistoryProductWindows.inheritedWidthline 20 - def
OAI.Ostmann.Arithmetic.HistoryProductWindows.removedWidthline 21 - theorem
OAI.Ostmann.Arithmetic.HistoryProductWindows.left_inherited_windowline 26 - theorem
OAI.Ostmann.Arithmetic.HistoryProductWindows.right_inherited_windowline 61 - theorem
OAI.Ostmann.Arithmetic.HistoryProductWindows.removed_windowline 96