mul_self_mul

Mathlib.Algebra.Group.Idempotent

URI: https://scilib.ai/kg/mathlib#IsIdempotentElem.mul_self_mul

← MathLib Explorer

English

If x is idempotent in a semigroup, then x multiplies with itself on the left by x, i.e., x * (x * y) = x * y for all y.

Русский

Если x идемпотентен, то x умножает себя слева над любым y: x * (x * y) = x * y.

LaTeX

$$$x * (x * y) = x * y$$$

Lean4

theorem mul_self_mul {M : Type*} [Semigroup M] {x : M} (hx : IsIdempotentElem x) (y : M) : x * (x * y) = x * y :=
  mul_assoc x x y ▸ congrArg (· * y) hx.eq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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