stabilizerEquivStabilizer_zero — Mathlib

English

The stabilizer equivalence for the zero orbit translation is the identity on stabilizers.

Русский

Эквивалентность стабилизаторов для нулевой орбиты равна тождественному отображению на стабилизаторах.

LaTeX

$$$\\text{stabilizerEquivStabilizer (zero\_vadd G a).symm} = \\mathrm{AddEquiv.refl} (\\mathrm{stabilizer} G a).$$$

Lean4

theorem stabilizerEquivStabilizer_zero :
    stabilizerEquivStabilizer (zero_vadd G a).symm = AddEquiv.refl (stabilizer G a) := by ext;
  simp [stabilizerEquivStabilizer_apply]

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