torsionMulEquiv — Mathlib

English

A torsion monoid is isomorphic to its torsion submonoid.

Русский

Торсионный моноид изоморфен своему торсионному подмоноиду.

LaTeX

$$$\operatorname{torsion} G \cong_* G$$$

Lean4

/-- A torsion monoid is isomorphic to its torsion submonoid. -/
@[to_additive /-- An additive torsion monoid is isomorphic to its torsion submonoid. -/
    ]
def torsionMulEquiv (tG : IsTorsion G) : torsion G ≃* G :=
  (MulEquiv.submonoidCongr tG.torsion_eq_top).trans Submonoid.topEquiv

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