smulShortComplex_shortExact — Mathlib

English

If r is regular on M, then the smulShortComplex is ShortExact.

Русский

Если r регулярно действует на M, то смул-штрих короткого комплекса является кратко точным.

LaTeX

$$$\text{If } \operatorname{IsSmulRegular}(M,r), \text{ then } (smulShortComplex(M,r)).ShortExact.$$$

Lean4

theorem smulShortComplex_shortExact {r : R} (reg : IsSMulRegular M r) : (ModuleCat.smulShortComplex M r).ShortExact
    where
  exact := ModuleCat.smulShortComplex_exact M r
  mono_f := by simpa [ModuleCat.smulShortComplex, ModuleCat.mono_iff_injective] using reg

Похожие утверждения