Commit 2025-06-15 16:47 5756ff47

View on Github →

feat(RingTheory/IsSMulRegular): categorical constructions for IsSMulRegular (#23935) The categorical constructions for IsSMulRegular for later use related to Ext in a separate file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/ExactSequence.lean

added theorem CategoryTheory.ComposableArrows.Exact.isIso_map'

Created Mathlib/RingTheory/Regular/Category.lean

added theorem IsSMulRegular.smulShortComplex_shortExact

added theorem LinearMap.exact_smul_id_smul_top_mkQ

added def ModuleCat.smulShortComplex

added theorem ModuleCat.smulShortComplex_exact