one_apply

Mathlib.Algebra.Order.Group.End

URI: https://scilib.ai/kg/mathlib#RelIso.one_apply

English

The action of the product on an element is given by applying the second then the first.

Русский

Действие произведения на элемент задаётся как последовательное применение второго затем первого.

LaTeX

$$$(e_1 * e_2) x = e_1\big( e_2 x\big)$$$

Lean4

theorem one_apply (x : α) : (1 : r ≃r r) x = x :=
  rfl

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

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

Разделы

Аффилиация

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