OAI/Algebra/FinitisticAsymmetry/Transport/FiniteModules.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LittleFinitistic.compactElement_orderIso line 17
2. lemma OAI.LittleFinitistic.moduleFinite_equivalence_iff line 28
3. lemma OAI.LittleFinitistic.littleFinitisticDimension_le_big line 42
4. lemma OAI.LittleFinitistic.littleFinitisticDimension_le_of_equivalence line 47
5. lemma OAI.LittleFinitistic.littleFinitisticDimension_equivalence line 58
6. lemma OAI.LittleFinitistic.bigFinitisticDimension_le_of_equivalence line 64
7. lemma OAI.LittleFinitistic.bigFinitisticDimension_equivalence line 73