act'_apply

Mathlib.Algebra.Quandle

URI: https://scilib.ai/kg/mathlib#Rack.act'_apply

English

The action act' coincides with the shelf operation: act'(x)(y) = x ◃ y.

Русский

Действие act'(x) совпадает с операцией полки: act'(x)(y) = x ◃ y.

LaTeX

$$$act'(x) y = x \triangleleft y$$$

Lean4

@[simp]
theorem act'_apply (x y : R) : act' x y = x ◃ y :=
  rfl

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

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

Разделы

Аффилиация

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