OAI/RingTheory/DirectFiniteness/ChosenCriterion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KaplanskyCounterexample.ChosenCriterion.inclusion line 21
2. abbrev OAI.KaplanskyCounterexample.ChosenCriterion.inclusion_injective line 22
3. abbrev OAI.KaplanskyCounterexample.ChosenCriterion.Extension line 23
4. abbrev OAI.KaplanskyCounterexample.ChosenCriterion.Group line 25
5. def OAI.KaplanskyCounterexample.ChosenCriterion.aOut line 31
6. def OAI.KaplanskyCounterexample.ChosenCriterion.bOut line 36
7. lemma OAI.KaplanskyCounterexample.ChosenCriterion.products line 42
8. instance OAI.KaplanskyCounterexample.ChosenCriterion.groupFG line 87