isMulTorsionFree_iff_not_isOfFinOrder

English

For a commutative group G, IsMulTorsionFree G is equivalent to the statement that every a ≠ 1 is not of finite order.

Русский

Для коммутативной группы G равносильны: IsMulTorsionFree G и то, что для каждого a ≠ 1 не имеет конечного порядка.

LaTeX

$$IsMulTorsionFree G ⇔ ∀ a ≠ 1, ¬IsOfFinOrder a$$

Lean4

@[to_additive]
theorem isMulTorsionFree_iff_not_isOfFinOrder : IsMulTorsionFree G ↔ ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a
    where
  mp _ _ := not_isOfFinOrder_of_isMulTorsionFree
  mpr
    hG := by
    refine ⟨fun n hn a b hab ↦ ?_⟩
    rw [← div_eq_one] at hab ⊢
    simp only [← div_pow, isOfFinOrder_iff_pow_eq_one] at hab hG
    exact of_not_not fun hab' ↦ hG hab' ⟨n, hn.bot_lt, hab⟩

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