OAI/RingTheory/DirectFiniteness/CandidateDependencies.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.SlabVariable line 13
2. abbrev OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.Occurrence line 18
3. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.occurrence_index_injective line 21
4. instance OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.(instance at line 28) line 28
5. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.occurrence_card line 32
6. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.occurrenceVariable line 49
7. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.occurrenceVector line 52
8. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.occurrenceVariable_injective line 54
9. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.deps line 73
10. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.deps_card line 75
11. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.deps_nonempty line 79
12. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.deps_card_le_four line 85
13. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.mem_deps_iff line 90
14. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.mem_deps_iff_rooted line 94
15. def OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.constraintVector line 117
16. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.constraintVector_at line 121
17. lemma OAI.KaplanskyCounterexample.FiniteGeometry.Candidate.constraintVector_nonzero line 128