Def ModuleCat.smulShortComplex

Modification history

2025-06-15 16:47

Mathlib/RingTheory/Regular/Category.lean

feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular (#23935) …

Added ModuleCat.smulShortComplex View on Github →