OAI/NumberTheory/Ostmann/Construction/CanonicalOccurrenceTransportPair.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.sameFibersEquiv line 11
2. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.sameFibersEquiv_apply line 27
3. abbrev OAI.Ostmann.Construction.CanonicalOccurrenceTransport.PairCoordinate line 33
4. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.canonicalPairMap line 35
5. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.canonicalPairMap_surjective line 40
6. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.coordinatePattern line 51
7. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.pairCoordinatePattern line 56
8. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.canonicalPairMap_val line 61
9. lemma OAI.Ostmann.Construction.CanonicalOccurrenceTransport.canonicalPairMap_eq_iff line 76
10. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.SamePairPattern line 88
11. def OAI.Ostmann.Construction.CanonicalOccurrenceTransport.pairKeyEquiv line 94
12. theorem OAI.Ostmann.Construction.CanonicalOccurrenceTransport.pairKeyEquiv_map line 103