isTorsionFree_iff_noZeroSMulDivisors_int

English

In an additive group, IsTorsionFree is equivalent to NoZeroSMulDivisors for integers.

Русский

В аддитивной группе IsTorsionFree эквивалентно NoZeroSMulDivisors для целых.

LaTeX

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

Lean4

@[deprecated noZeroSMulDivisors_int_iff_isAddTorsionFree (since := "2025-04-23")]
theorem isTorsionFree_iff_noZeroSMulDivisors_int [SubtractionMonoid G] : IsTorsionFree G ↔ NoZeroSMulDivisors ℤ G :=
  by
  simp_rw [AddMonoid.IsTorsionFree, isOfFinAddOrder_iff_zsmul_eq_zero, not_exists, not_and, noZeroSMulDivisors_iff,
    forall_swap (β := ℤ)]
  exact forall₂_congr fun _ _ ↦ by tauto

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