Theorem CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁

Modification history

2025-10-02 11:57
Mathlib/CategoryTheory/Abelian/Injective/Dimension.lean
feat(Algebra/Homology): add injective dimension (#30080) …
Added CategoryTheory.ShortComplex.ShortExact.hasInjectiveDimensionLT_X₁View on Github →