torsion_eq_top — Mathlib

English

The torsion submonoid of a torsion monoid is the top submonoid; i.e., every element lies in the torsion submonoid.

Русский

Торсионная подмоноида торсионного моноида равна верхнему подмоноиду; то есть каждый элемент принадлежит торсионной подмоноиде.

LaTeX

$$$\text{torsion } G = \top$ when $G$ is a torsion monoid.$$

Lean4

/-- The torsion submonoid of a torsion monoid is `⊤`. -/
@[to_additive (attr := simp) /-- The additive torsion submonoid of an additive torsion monoid is `⊤`. -/
    ]
theorem torsion_eq_top (tG : IsTorsion G) : torsion G = ⊤ := by ext; tauto

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