OAI/NumberTheory/Ostmann/Construction/CanonicalHistory.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Ostmann.Construction.AllowedFrequency line 11
2. def OAI.Ostmann.Construction.HistoryChoices line 14
3. instance OAI.Ostmann.Construction.historyChoicesFintype line 20
4. def OAI.Ostmann.Construction.decodedPivot line 29
5. def OAI.Ostmann.Construction.decodeHistory line 35
6. theorem OAI.Ostmann.Construction.decodeHistory_root line 51
7. def OAI.Ostmann.Construction.choicesMass line 56
8. theorem OAI.Ostmann.Construction.decodeHistory_internalMass line 63
9. def OAI.Ostmann.Construction.canonicalCoefficient line 72