OAI/RingTheory/DirectFiniteness/CandidateBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.TwoCode.equiv line 16
2. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.twoCode_card line 23
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.oneCode_card_le line 30
4. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.two_rooted_card_le line 43
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.one_rooted_card_le line 52
6. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.local_card_le_rooted line 62
7. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.local_one_card_le line 72
8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.local_two_card_le line 78