stabilizerEquivStabilizer_trans — Mathlib

English

The composition of stabilizer equivalences along consecutive orbit steps equals the stabilizer equivalence along the combined step.

Русский

Составления эквивалентностей стабилизаторов по последовательным шагам орбиты равны эквивалентности по суммарному шагу.

LaTeX

$$$\\bigl(\\mathrm{stabilizerEquivStabilizer } hg\\bigr).\\mathrm{trans} (\\mathrm{stabilizerEquivStabilizer } hh) = \\mathrm{stabilizerEquivStabilizer } hk.$$$

Lean4

theorem stabilizerEquivStabilizer_trans (hg : b = g +ᵥ a) (hh : c = h +ᵥ b) (hk : c = k +ᵥ a) (H : k = h + g) :
    (stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = stabilizerEquivStabilizer hk := by ext;
  simp [stabilizerEquivStabilizer_apply, H]

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