conj_injective — Mathlib

English

For a fixed element x in a group, the map g ↦ x g x^{-1} is injective: if x g x^{-1} = x h x^{-1}, then g = h.

Русский

Для фиксированного элемента x в группе отображение g ↦ x g x^{-1} инъективно: если x g x^{-1} = x h x^{-1}, то g = h.

LaTeX

$$$\forall g,h \in \alpha,\ x g x^{-1} = x h x^{-1} \Rightarrow g = h$$$

Lean4

theorem conj_injective {x : α} : Function.Injective fun g : α => x * g * x⁻¹ :=
  (MulAut.conj x).injective

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