conj_mk — Mathlib

English

In any group, a semiconjugates x to a x a^{-1}.

Русский

В любой группе элемент a полусопрягает x к a x a^{-1}.

LaTeX

$$$$\text{For } a,x\in G:\ SemiconjBy\ a\ x\ (a\,x\,a^{-1}).$$$$

Lean4

/-- `a` semiconjugates `x` to `a * x * a⁻¹`. -/
@[to_additive /-- `a` semiconjugates `x` to `a + x + -a`. -/
    ]
theorem conj_mk (a x : G) : SemiconjBy a x (a * x * a⁻¹) := by unfold SemiconjBy;
  rw [mul_assoc, inv_mul_cancel, mul_one]

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