OAI/Algebra/FinitisticAsymmetry/Transport/ScalarRestriction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.LittleFinitistic.restrictScalars_preservesFiniteLimits line 20
2. instance OAI.LittleFinitistic.restrictScalars_preservesFiniteColimits line 24
3. lemma OAI.LittleFinitistic.restrictScalars_full line 28
4. lemma OAI.LittleFinitistic.restrictScalars_preservesProjectives line 37
5. lemma OAI.LittleFinitistic.finite_restrictScalars line 56
6. lemma OAI.LittleFinitistic.littleFinitisticDimension_le_restrictScalars line 74
7. lemma OAI.LittleFinitistic.bigFinitisticDimension_le_restrictScalars line 88