not_isOfFinOrder_of_isMulTorsionFree

English

Let G be a monoid with IsMulTorsionFree. If a ≠ 1, then a has infinite order.

Русский

Пусть G — моноид с условием безторсионности. Если a ≠ 1, то a имеет бесконечный порядок.

LaTeX

$$$IsMulTorsionFree G \\land a \\neq 1 \\Rightarrow \\neg IsOfFinOrder a$$$

Lean4

@[to_additive]
theorem not_isOfFinOrder_of_isMulTorsionFree [IsMulTorsionFree G] (ha : a ≠ 1) : ¬IsOfFinOrder a :=
  by
  rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨n, hn, han⟩
  exact ha <| pow_left_injective hn.ne' <| by simpa using han

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