OAI/NumberTheory/Ostmann/Construction/InitialCoordinatesTemplateIndex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.initialRoles_length line 10
2. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.initial_length line 15
3. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.matches_initial_length line 19
4. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.initialRoles_bulk_iff line 23
5. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.matches_initial_metadata line 47
6. def OAI.Ostmann.Construction.InitialCoordinatesTemplate.halfEquiv line 59
7. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.halfEquiv_val line 62
8. def OAI.Ostmann.Construction.InitialCoordinatesTemplate.compensationEquiv line 66
9. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.compensationEquiv_val line 70
10. abbrev OAI.Ostmann.Construction.InitialCoordinatesTemplate.SmallShape line 76
11. def OAI.Ostmann.Construction.InitialCoordinatesTemplate.smallEquiv line 78
12. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.smallEquiv_bulk_val line 83
13. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.smallEquiv_top_val line 87
14. theorem OAI.Ostmann.Construction.InitialCoordinatesTemplate.smallEquiv_compensation_val line 93