OAI/RingTheory/DirectFiniteness/PrescribedSlots.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.Prescription.slotPairOrder line 15
2. def OAI.KaplanskyCounterexample.Prescription.slotAssignment line 21
3. lemma OAI.KaplanskyCounterexample.Prescription.slotAssignment_rank line 39

   Source documentation

   The assigned pair has exactly the point's rank in the finite order, so the image consists of the first t pairs, with none skipped or repeated.

   lemma slotAssignment_rank (hsize : Fintype.card V ≤ Fintype.card m * ℓ^2) (v : V) :
       letI := slotPairOrder (m := m) ℓ
   …

   Mentions: OAI.KaplanskyCounterexample.Prescription.slotPairOrder

4. lemma OAI.KaplanskyCounterexample.Prescription.slotAssignment_first_pairs line 47
5. def OAI.KaplanskyCounterexample.Prescription.assignedSlot line 66
6. def OAI.KaplanskyCounterexample.Prescription.assignedForm line 69
7. lemma OAI.KaplanskyCounterexample.Prescription.assignedForm_distinct line 73