stabilizerEquivStabilizer_apply — Mathlib

English

Same as above: the stabilizer equivalence sends an element by conjugation with the associated group element.

Русский

То же утверждение: изображение через конъюгацию соответствующего элемента группы.

LaTeX

$$$\\text{stabilizerEquivStabilizer } hg\\; x = (\\mathrm{AddAut.conj } g).\\toMul x.$$$

Lean4

theorem stabilizerEquivStabilizer_apply (hg : b = g +ᵥ a) (x : stabilizer G a) :
    stabilizerEquivStabilizer hg x = (AddAut.conj g).toMul x := by simp [stabilizerEquivStabilizer]

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