isTorsionFree_iff_noZeroSMulDivisors_nat

English

A group is torsion-free if and only if NoZeroSMulDivisors for integers holds (Int module).

Русский

Безторсионность эквивалентна свойству NoZeroSMulDivisors над целыми.

LaTeX

$$$IsTorsionFree G \iff NoZeroSMulDivisors \mathbb{Z} G$$$

Lean4

@[deprecated noZeroSMulDivisors_nat_iff_isAddTorsionFree (since := "2025-04-23")]
theorem isTorsionFree_iff_noZeroSMulDivisors_nat {M : Type*} [AddMonoid M] : IsTorsionFree M ↔ NoZeroSMulDivisors ℕ M :=
  by
  simp_rw [AddMonoid.IsTorsionFree, isOfFinAddOrder_iff_nsmul_eq_zero, not_exists, not_and, pos_iff_ne_zero,
    noZeroSMulDivisors_iff, forall_swap (β := ℕ)]
  exact forall₂_congr fun _ _ ↦ by tauto

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