OAI/RingTheory/DirectFiniteness/AffineLines.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.mem_linePoints line 13
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.linePoints_rebase line 17
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.linePoints_scale line 23
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.FullLine.eq_linePoints_sub line 31
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.FullLine.eq_of_two_mem line 44
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.direction_sub_mem line 50
7. structure OAI.KaplanskyCounterexample.FiniteGeometry.LinePartition line 60

   Source documentation

   A partition by full lines, represented without arbitrary labels or duplicates.

   structure LinePartition where
   …

8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.LinePartition.mem_iff line 69
9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.LinePartition.disjoint_or_eq line 72