IsTorsion — Mathlib

English

IsTorsion G is defined as every element of G has finite order.

Русский

IsTorsion G трактуется как: каждый элемент группы имеет конечный порядок.

LaTeX

$$$\text{IsTorsion}(G) \;\equiv\; \forall g\in G\;\text{IsOfFinOrder}(g)$$$

Lean4

/-- A predicate on a monoid saying that all elements are of finite order. -/
@[to_additive /-- A predicate on an additive monoid saying that all elements are of finite order. -/
    ]
def IsTorsion :=
  ∀ g : G, IsOfFinOrder g

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