noZeroSMulDivisors_int_iff_isAddTorsionFree

English

For an AddCommGroup G, NoZeroSMulDivisors Int G is equivalent to IsAddTorsionFree G.

Русский

Для абелевой группы G с IsAddTorsionFree верно NoZeroSMulDivisors ℤ G ⇔ IsAddTorsionFree G.

LaTeX

$$$$\text{NoZeroSMulDivisors}(\mathbb{Z}, G) \iff \text{IsAddTorsionFree}(G).$$$$

Lean4

@[simp]
theorem noZeroSMulDivisors_int_iff_isAddTorsionFree [AddCommGroup G] : NoZeroSMulDivisors ℤ G ↔ IsAddTorsionFree G
    where
  mp
    _ := by
    refine ⟨fun n hn a b hab ↦ ?_⟩
    simp only [← sub_eq_zero (a := (n : ℤ) • a), ← zsmul_sub, ← natCast_zsmul] at hab
    simpa [sub_eq_zero] using (smul_eq_zero_iff_right <| Int.natCast_ne_zero.2 hn).1 hab
  mpr _ := inferInstance

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