OAI/NumberTheory/Ostmann/Arithmetic/HistorySignedResidueFactorizationBasic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.RootFrequencyGiantCoprime line 13
2. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.FrequencyGiantCoprime line 17
3. def OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.PivotOutsideCoprime line 23
4. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization._root_.OAI.Ostmann.Arithmetic.HistorySignedSpectator.OutsideUnits.pivotOutsideCoprime line 29
5. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.currentGiantUnits_of_frequencyGiantCoprime line 36
6. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.rootArithmetic_rebuild_iff line 55
7. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.numeratorSquares_node_iff line 64
8. theorem OAI.Ostmann.Arithmetic.HistorySignedResidueFactorization.arithmeticGuards_rebuild_iff line 85