quandle — Mathlib

English

For any group G, the set Conj G with operation x ◃ y := y^{-1} x y forms a quandle.

Русский

Для группы G множество Conj G с операцией x ◃ y := y^{-1} x y образует квардлу.

LaTeX

$$$x \triangleleft y = y^{-1} x y$$$

Lean4

instance quandle (G : Type*) [Group G] : Quandle (Conj G)
    where
  act x := @MulAut.conj G _ x
  self_distrib := by
    intro x y z
    dsimp only [MulAut.conj_apply]
    simp [mul_assoc]
  invAct x := (@MulAut.conj G _ x).symm
  left_inv x y := by simp [mul_assoc]
  right_inv x y := by simp [mul_assoc]
  fix := by simp

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