units — Mathlib

English

Given a subgroup S of Mˣ, its image under the natural inclusion is a submonoid of M.

Русский

Для подгруппы S в Mˣ её образ через естественное включение является подмоном в M.

LaTeX

$$S^{\\circ} := S.\\text{ofUnits} \\text{ is a Submonoid of } M$$

Lean4

/-- The units of `S`, packaged as a subgroup of `Mˣ`. -/
@[to_additive /-- The additive units of `S`, packaged as an additive subgroup of `AddUnits M`. -/
    ]
def units (S : Submonoid M) : Subgroup Mˣ
    where
  toSubmonoid := S.comap (coeHom M) ⊓ (S.comap (coeHom M))⁻¹
  inv_mem' ha := ⟨ha.2, ha.1⟩

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