Theorem IsSMulRegular.smulShortComplex_shortExact

Modification history

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