instCommGroupSubtypeMemSubmonoid — Mathlib

English

For any x ∈ IsUnit.submonoid M, the natural inclusion sends x^{-1} to the inverse in M, i.e., the image of x^{-1} equals the inverse of the image x.

Русский

Для любого x ∈ IsUnit.submonoid M, образ x^{-1} в M совпадает с обратным элементом к образу x.

LaTeX

$$For x ∈ IsUnit.submonoid M, ↑x^{-1} = (↑x.prop.unit^{-1} : M).$$

Lean4

@[to_additive]
noncomputable instance [CommMonoid M] : CommGroup (IsUnit.submonoid M) :=
  { inferInstanceAs (Group (IsUnit.submonoid M)) with mul_comm := fun a b ↦ by convert mul_comm a b }

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