mk_mul_mk_inv_eq_one — Mathlib

English

Let S be a submonoid of a monoid M. If x is a unit of M and x lies in S, then the element of S corresponding to x, multiplied by the element corresponding to x^{-1}, equals the identity of S.

Русский

Пусть S — подмоноид моноидов M. Если x — единица M и x ∈ S, то соответствующая x в S единица умножения на соответствующую x^{-1} даёт единицу S.

LaTeX

$$$ (\langle x, h.1 \rangle : S) \cdot \langle x^{-1}, h.2 \rangle = 1_S $$$

Lean4

@[to_additive]
theorem mk_mul_mk_inv_eq_one (S : Submonoid M) {x : Mˣ} (h : x ∈ S.units) : (⟨_, h.1⟩ : S) * ⟨_, h.2⟩ = 1 :=
  Subtype.ext x.mul_inv

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