noZeroSMulDivisors_nat_iff_isAddTorsionFree

English

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

Русский

Для абелевой группы G с дополнением кAddCommGroup нулевые делители под ℕ эквивалентны IsAddTorsionFree G.

LaTeX

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

Lean4

@[simp]
theorem noZeroSMulDivisors_nat_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), ← nsmul_sub] at hab
    simpa [sub_eq_zero] using (smul_eq_zero_iff_right hn).1 hab
  mpr _ := inferInstance

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