instIsTorsionFreeNatOfIsAddTorsionFree

English

Let M be an additive commutative monoid with a natural-number (ℕ) module structure. If M is additively torsion-free, then the action of ℕ on M is torsion-free; equivalently, for all m ∈ M and n ∈ ℕ with n ≠ 0, n · m = 0 implies m = 0.

Русский

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

LaTeX

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

Lean4

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

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