conj_swap — Mathlib

English

For group G, and x,y in Conj G, x ◃ y = y ↔ y ◃ x = x; i.e., symmetry of the conjugation operation.

Русский

Для группы G и элементов x,y из Conj G, x ◃ y = y ↔ y ◃ x = x; то есть симметрия операции конъюгации.

LaTeX

$$$x \triangleleft y = y \iff y \triangleleft x = x$$$

Lean4

theorem conj_swap {G : Type*} [Group G] (x y : Conj G) : x ◃ y = y ↔ y ◃ x = x :=
  by
  dsimp [Conj] at *; constructor
  repeat' intro h; conv_rhs => rw [eq_mul_inv_of_mul_eq (eq_mul_inv_of_mul_eq h)]; simp

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