unitsEquivSelf — Mathlib

English

There is a natural equivalence between the units of H and H itself.

Русский

Существует естественное эквивалентное соответствие между единицами H и самим H.

LaTeX

$$$H^{\\mathrm{units}} \\cong_* H$$$

Lean4

/-- The equivalence between the greatest subgroup of units contained within `T` and `T` itself. -/
@[to_additive /-- The equivalence between the greatest subgroup of additive units
    contained within `T` and `T` itself. -/
    ]
def unitsEquivSelf (H : Subgroup G) : H.units ≃* H :=
  H.unitsEquivUnitsType.trans (toUnits (G := H)).symm

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