OrdinaryProductDimension.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.LittleFinitistic.ProductModules.firstInflation_preservesHomology line 13
Source documentation
Exactness of actual inflation, with the module universe independent of the ring universe.
```
theorem firstInflation_preservesHomology :
    (firstInflation.{u,v} L R).PreservesHomology :=
…
```
theorem OAI.LittleFinitistic.ProductModules.firstInflation_dimensionLE line 21
Source documentation
Inflation from a factor preserves finite projective-dimension bounds, via actual projective covers.
```
theorem firstInflation_dimensionLE (n : ℕ) (M : ModuleCat.{v} L) [HasProjectiveDimensionLE M n] :
    HasProjectiveDimensionLE ((firstInflation L R).obj M) n := by
…
```
Mentions: OAI.LittleFinitistic.ProductModules.firstInflation