minOrder_eq_top — Mathlib

English

If G is torsion-free (no nontrivial finite-order elements), then minOrder G equals the top element, i.e., ∞.

Русский

Если группа G тензорно безциклична (нет ненулевых элементов конечного порядка), то minOrder G равно верхнему элементу, т.е. бесконечности.

LaTeX

$$$[IsMulTorsionFree\ G]\Rightarrow \minOrder G = \top$$$

Lean4

@[to_additive (attr := simp)]
theorem minOrder_eq_top [IsMulTorsionFree G] : minOrder G = ⊤ := by
  simpa [minOrder] using fun _ ↦ not_isOfFinOrder_of_isMulTorsionFree

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