not_isTorsion_iff — Mathlib

English

A monoid is not torsion if and only if there exists an element of infinite order.

Русский

Моноид не тождественен к торсии тогда и только тогда, когда существует элемент бесконечного порядка.

LaTeX

$$$\neg\ IsTorsion(G) \ \Leftrightarrow\ \exists g\in G, \neg IsOfFinOrder(g)$$$

Lean4

/-- A monoid is not a torsion monoid if it has an element of infinite order. -/
@[to_additive (attr := simp) /-- An additive monoid is not a torsion monoid if it
      has an element of infinite order. -/
    ]
theorem not_isTorsion_iff : ¬IsTorsion G ↔ ∃ g : G, ¬IsOfFinOrder g := by rw [IsTorsion, not_forall]

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