conj_act_eq_conj — Mathlib

English

In the conjugation quandle on Conj G, the operation x ◃ y is given by conjugation by x on y, i.e., x ◃ y = (x y x^{-1}) in G.

Русский

В квардле сопряжения на Conj G операция x ◃ y задаётся конъюгацией: x ◃ y = x y x^{-1} (в G).

LaTeX

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

Lean4

@[simp]
theorem conj_act_eq_conj {G : Type*} [Group G] (x y : Conj G) : x ◃ y = ((x : G) * (y : G) * (x : G)⁻¹ : G) :=
  rfl

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