mul_mul_self

Mathlib.Algebra.Group.Idempotent

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

← MathLib Explorer

English

In a semigroup, for hx : IsIdempotentElem x and any y, we have y x x = y x.

Русский

В полугруппе для идемпотентного элемента x и любого y верно y x x = y x.

LaTeX

$$$y \\cdot x \\cdot x = y \\cdot x.$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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