Theorem ModuleCat.smulShortComplex_exact

Modification history

2025-06-15 16:47
Mathlib/RingTheory/Regular/Category.lean
feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular (#23935) …
Added ModuleCat.smulShortComplex_exactView on Github →