mul_fromLeftInv

Mathlib.GroupTheory.Submonoid.Inverses

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

English

In a commutative monoid, (S.fromLeftInv x) · x = 1 for any x ∈ S.leftInv.

Русский

В коммутативном моноиде, для любого x ∈ S.leftInv, (S.fromLeftInv x) · x = 1.

LaTeX

$$For x ∈ S.leftInv, (S.fromLeftInv x) · x = 1.$$

Lean4

@[to_additive (attr := simp)]
theorem mul_fromLeftInv (x : S.leftInv) : (x : M) * S.fromLeftInv x = 1 :=
  x.prop.choose_spec

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

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

Разделы

Аффилиация

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