OAI/RingTheory/DirectFiniteness/SlabHoleEvents.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.diff_mem_coset line 15
2. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.LocalHolePair line 20
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.localHolePair_card line 23
4. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.localHolePairVector line 29
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.localHolePairVector_eq line 33
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.localHolePairVector_nonzero line 38