instGroupSubtypeMemSubmonoid — Mathlib

English

If M is commutative, then IsUnit.submonoid M has a commutative group structure.

Русский

Если M коммутативен, то IsUnit.submonoid M является коммутативной группой.

LaTeX

$$[Monoid M is CommMonoid] ⇒ IsUnit.submonoid M is a CommGroup.$$

Lean4

@[to_additive]
noncomputable instance [Monoid M] : Group (IsUnit.submonoid M) :=
  {
    inferInstanceAs
      (Monoid (IsUnit.submonoid
          M)) with
    inv := fun x ↦ ⟨x.prop.unit⁻¹.val, x.prop.unit⁻¹.isUnit⟩
    inv_mul_cancel := fun x ↦ Subtype.ext ((Units.val_mul x.prop.unit⁻¹ _).trans x.prop.unit.inv_val) }

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