OAI/RingTheory/DirectFiniteness/PrescribedDirections.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Prescription.directionSet line 15

   Source documentation

   A direction is ordered by its full underlying point set. Slopes are just coordinates for all of the one-dimensional subspaces, including the vertical one.

   def directionSet (d : Option (ZMod ℓ)) : Finset (Fin 2 → ZMod ℓ) :=
   …

2. lemma OAI.KaplanskyCounterexample.Prescription.directionSet_injective line 18
3. def OAI.KaplanskyCounterexample.Prescription.directionOrder line 28
4. lemma OAI.KaplanskyCounterexample.Prescription.direction_first line 33
5. lemma OAI.KaplanskyCounterexample.Prescription.direction_first_nonzero line 64
6. lemma OAI.KaplanskyCounterexample.Prescription.direction_range_finrank line 68
7. def OAI.KaplanskyCounterexample.Prescription.orderedAssignment line 72