instIsTorsionFreeIntOfIsAddTorsionFree

English

Let M be an additive abelian group with a ℤ-module structure. If M is additively torsion-free, then M is torsion-free as a ℤ-module; equivalently, for all m ∈ M and n ∈ ℤ with n ≠ 0, n · m = 0 implies m = 0.

Русский

Пусть M — абелева группа с действием по кольцу целых чисел. Если M безторсионна относительно сложения, то и как модуль над ℤ безторсионна: для всех m ∈ M и n ∈ ℤ с n ≠ 0, n · m = 0 ⇒ m = 0.

LaTeX

$$$\text{IsAddTorsionFree}(M) \Rightarrow \text{IsTorsionFree}_{\mathbb{Z}}(M)$$$

Lean4

instance [IsAddTorsionFree M] : IsTorsionFree ℤ M where
  isSMulRegular n hn := zsmul_right_injective (by simpa [isRegular_iff_ne_zero] using hn)

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