OAI/RingTheory/DirectFiniteness/OneCandidateCounting.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KaplanskyCounterexample.FiniteGeometry.one_position_recovery line 14
2. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode line 34
3. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.other line 38
4. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.idx line 39
5. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.tag line 40
6. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.point line 41
7. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.nextPoint line 42
8. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.exc line 43
9. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.lab line 45
10. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.OneCode.known line 47
11. structure OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.CoveredOne line 52
12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.CoveredOne.unique line 59
13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.one_label_codec line 72