We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent cb6a455 commit b6fa447Copy full SHA for b6fa447
Mathlib/RingTheory/Regular/Category.lean
@@ -33,7 +33,6 @@ lemma LinearMap.exact_lsmul_smul_top_mkQ (M : Type v) [AddCommGroup M] [Module R
33
namespace ModuleCat
34
35
/-- The short (exact) complex `M → M → M⧸xM` obtain from the scalar multiple of `x : R` on `M`. -/
36
-@[simps]
37
def smulShortComplex (r : R) : ShortComplex (ModuleCat R) :=
38
ModuleCat.shortComplexOfCompEqZero (LinearMap.lsmul _ M r) (r • (⊤ : Submodule R M)).mkQ
39
(LinearMap.exact_lsmul_smul_top_mkQ M r).linearMap_comp_eq_zero
0 commit comments