mk_inv_mul_mk_eq_one

Mathlib.Algebra.Group.Submonoid.Units

URI: https://scilib.ai/kg/mathlib#Submonoid.mk_inv_mul_mk_eq_one

English

For S a Submonoid and x ∈ S.units, the product of the pair (x⁻¹, x) as elements of S is the identity in S.

Русский

Для S ⊆ M и x ∈ S.units произведение пары (x⁻¹, x) в S равно единице в S.

LaTeX

$$$(⟨_, x⟩ : S) * ⟨_, x⁻¹⟩ = 1$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru