OAI/RingTheory/DirectFiniteness/CandidateCounting.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.card_le_of_unique_cover line 13
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.pair_set_of_card_two line 21
3. structure OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.Rooted line 34
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.Rooted.ext line 41
5. instance OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.Rooted.(instance at line 43) line 43
6. structure OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.TwoCode line 51

   Source documentation

   A deliberately generous finite codec. The last field stores k exceptional scalars rather than just one; the final numeric load still tends to zero.

   structure TwoCode where
   …

7. instance OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.(instance at line 60) line 60
8. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.TwoCode.lab line 67
9. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.TwoCode.known line 70
10. structure OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.CoveredTwo line 74
11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.CoveredTwo.unique line 83
12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.two_label_codec line 105