topEquiv — Mathlib

English

The top subgroup is isomorphic to the group via a multiplicative equivalence.

Русский

Верхняя подгруппа изоморфна группе через мультипликативное эквивалентное отображение.

LaTeX

$$$$ (\\top : \\mathrm{Subgroup}(G)) \\cong_* G. $$$$

Lean4

/-- The top subgroup is isomorphic to the group.

This is the group version of `Submonoid.topEquiv`. -/
@[to_additive (attr := simps!) /-- The top additive subgroup is isomorphic to the additive group.

          This is the additive group version of `AddSubmonoid.topEquiv`. -/
    ]
def topEquiv : (⊤ : Subgroup G) ≃* G :=
  Submonoid.topEquiv

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