module_of_torsion — Mathlib

English

If R is a torsion ring and M is a module over R, then M is a torsion module.

Русский

Если R — кольцо торовости и M — R-модуль, то M является торовым модулем.

LaTeX

$$IsTorsion M$$

Lean4

/-- A module whose scalars are additively torsion is additively torsion. -/
theorem module_of_torsion [Semiring R] [Module R M] (tR : IsTorsion R) : IsTorsion M := fun f =>
  isOfFinAddOrder_iff_nsmul_eq_zero.mpr <|
    by
    obtain ⟨n, npos, hn⟩ := (tR 1).exists_nsmul_eq_zero
    exact ⟨n, npos, by simp only [← Nat.cast_smul_eq_nsmul R _ f, ← nsmul_one, hn, zero_smul]⟩

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