not_isOfFinOrder_of_injective_pow

English

For a commutative group G, minOrder G equals top if and only if G is torsion-free.

Русский

Для коммутативной группы G minOrder G равно верхнему элементу тогда и только тогда, когда G не имеет конечного порядка элементов (torsion-free).

LaTeX

$$$\minOrder G = \top \iff IsMulTorsionFree G$$$

Lean4

/-- See also `injective_pow_iff_not_isOfFinOrder`. -/
@[to_additive /-- See also `injective_nsmul_iff_not_isOfFinAddOrder`. -/
    ]
theorem not_isOfFinOrder_of_injective_pow {x : G} (h : Injective fun n : ℕ => x ^ n) : ¬IsOfFinOrder x :=
  by
  simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
  intro n hn_pos hnx
  rw [← pow_zero x] at hnx
  rw [h hnx] at hn_pos
  exact irrefl 0 hn_pos

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