act_idem

Mathlib.Algebra.Quandle

URI: https://scilib.ai/kg/mathlib#UnitalShelf.act_idem

English

In a unital shelf, for every element x, the action of x on itself fixes x: x ◃ x = x.

Русский

В унитальной полке для каждого элемента x выполняется действие x на x: x ◃ x = x.

LaTeX

$$$x \triangleleft x = x$$$

Lean4

theorem act_idem (x : S) : (x ◃ x) = x := by rw [← act_one x, ← Shelf.self_distrib, act_one]

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

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

Разделы

Аффилиация

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