invAct_apply

Mathlib.Algebra.Quandle

URI: https://scilib.ai/kg/mathlib#Rack.invAct_apply

English

The inverse of act' x acts on y by x ◃⁻¹ y: (act' x)⁻¹ y = x ◃⁻¹ y.

Русский

Обратное к x действует на y как x ◃⁻¹ y: (act' x)⁻¹ y = x ◃⁻¹ y.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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