act'_symm_apply

Mathlib.Algebra.Quandle

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

English

The inverse action satisfies (act' x)^{-1} y = x ◃⁻¹ y for all x,y.

Русский

Обратное действие удовлетворяет (act' x)^{-1} y = x ◃⁻¹ y для всех x,y.

LaTeX

$$$(act'(x))^{-1} y = x \triangleleft^{-1} y$$$

Lean4

@[simp]
theorem act'_symm_apply (x y : R) : (act' x).symm y = x ◃⁻¹ y :=
  rfl

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

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

Разделы

Аффилиация

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