OAI/NumberTheory/Ostmann/Construction/CanonicalOccurrenceTransportNormalized.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.ofFn_finCongr line 10
2. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.fixedRootCode line 15
3. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.fixedCompensationCode line 18
4. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.root_code_normalized line 25
5. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.compensation_code_fixed line 37
6. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.compensation_code_normalized line 51
7. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.normalizedCode line 64
8. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.normalizedCode_eq_execute line 69