OAI/RingTheory/DirectFiniteness/HoleEvents.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_sup_le_mul line 11
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_bounded_tuples line 22
3. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.PairIndex line 44
4. instance OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.(instance at line 45) line 45
5. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.pairSet line 47
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.pairSet_card line 50
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.card_source_fiber line 54
8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.pairIndex_card line 65
9. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.OccupancyIndex line 78
10. instance OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.(instance at line 80) line 80
11. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.occupancySet line 83
12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.occupancySet_card line 87
13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.occupancyIndex_card line 92
14. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.corner line 107

    Source documentation

    Four cyclic corners, with side labels r,r',r,r'.

    def corner (e : R → Q → A) (r r' : R) (x : A) (u v : Q) : Fin 4 → A :=
    …

15. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.sideLabel line 110
16. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.RectangleIndex line 112
17. instance OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.(instance at line 115) line 115
18. def OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.rectangleSet line 118
19. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.rectangleSet_card line 122
20. lemma OAI.KaplanskyCounterexample.FiniteGeometry.HoleEvents.rectangleIndex_card line 127