Commit 2026-05-10 09:03 835f8a39

View on Github →

feat(RingTheory): refactor smulShortComplex (#37355) Use LinearMap.lsmul for the f of ModuleCat.smulShortComplex, also providing new APIs for it.

Estimated changes

Modified Mathlib/RingTheory/Regular/Category.lean

added theorem LinearMap.exact_lsmul_mkQ_smul_top

deleted theorem LinearMap.exact_smul_id_smul_top_mkQ

modified def ModuleCat.smulShortComplex

modified theorem ModuleCat.smulShortComplex_exact

added theorem ModuleCat.smulShortComplex_f_eq_smul_id