stabilizerEquivStabilizer_neg — Mathlib

English

If b equals −g plus a, the stabilizer equivalence corresponds to conjugation by −g.

Русский

Если $b = -g + a$, соответствующая эквивалентность стабилизаторов соответствует конъюгации на −g.

LaTeX

$$$\\text{stabilizerEquivStabilizer } (hg) = (\\text{stabilizerEquivStabilizer (neg\_vadd\_eq\_iff.mp hg.symm)}).symm.$$$

Lean4

theorem stabilizerEquivStabilizer_neg (hg : b = -g +ᵥ a) :
    stabilizerEquivStabilizer hg = (stabilizerEquivStabilizer (neg_vadd_eq_iff.mp hg.symm)).symm := by ext;
  simp [stabilizerEquivStabilizer]

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