Theorem ModuleCat.smulShortComplex_f_eq_smul_id

Modification history

2026-05-10 09:03
Mathlib/RingTheory/Regular/Category.lean
feat(RingTheory): refactor `smulShortComplex` (#37355) …
Added ModuleCat.smulShortComplex_f_eq_smul_idView on Github →