fromLeftInv_mul

Mathlib.GroupTheory.Submonoid.Inverses

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

English

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

Русский

В коммутативном моноиде fromLeftInv x · x = 1 при x ∈ S.leftInv.

LaTeX

$$If M is commutative, then for x ∈ S.leftInv, (S.fromLeftInv x) · x = 1.$$

Lean4

@[to_additive (attr := simp)]
theorem fromLeftInv_mul (x : S.leftInv) : (S.fromLeftInv x : M) * x = 1 := by rw [mul_comm, mul_fromLeftInv]

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

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

Разделы

Аффилиация

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