smulShortComplex_exact — Mathlib

English

For any r in a commutative ring R and any module M, the short complex associated to multiplication by r is exact.

Русский

Для любого элемента r∈R и модуля M соответствующий короткий комплекс, связанный с умножением на r, точен.

LaTeX

$$$\text{The short complex }(smulShortComplex(M,r))\text{ is exact.}$$$

Lean4

theorem smulShortComplex_exact (r : R) : (smulShortComplex M r).Exact := by
  simp [smulShortComplex, ShortComplex.ShortExact.moduleCat_exact_iff_function_exact,
    LinearMap.exact_smul_id_smul_top_mkQ]

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