OAI/RingTheory/DirectFiniteness/TradeLines.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.coset_range_eq_line line 15
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.coset_range_full line 25
3. def OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.replacementLine line 30
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.mem_replacementLine line 34
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.replacementLine_full line 50
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.replacementLine_subset line 54
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.replacementLine_hole_free line 61
8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.replacementLine_same_label line 73
9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.DirectionFrame.replacementLine_step line 88