OAI/RingTheory/DirectFiniteness/PartialPartition.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.image_linePoints line 14
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.image_affine_linePoints line 26
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.FullLine.image_affine line 41
4. structure OAI.KaplanskyCounterexample.FiniteGeometry.PartitionOn line 49

   Source documentation

   A full-line partition of one finite affine slab.

   structure PartitionOn (S : Finset A) where
   …

5. def OAI.KaplanskyCounterexample.FiniteGeometry.PartitionOn.parametrization line 61
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PartitionOn.parametrization_val line 70
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PartitionOn.parametrization_symm_apply line 73
8. def OAI.KaplanskyCounterexample.FiniteGeometry.PartitionOn.image line 77
9. lemma OAI.KaplanskyCounterexample.FiniteGeometry.PartitionOn.image_through line 95
10. def OAI.KaplanskyCounterexample.FiniteGeometry.gluePartition line 108