stabilizerEquivStabilizer_trans — Mathlib

English

If b = g • a, h • b = c, c = k • a, and k = h g, then the composition equals stabilizerEquivStabilizer hk.

Русский

Если b = g • a, c = h • b, c = k • a и k = h g, то композиция стабилизаторных эквивравельностей равна stabilizerEquivStabilizer hk.

LaTeX

$$(stabilizerEquivStabilizer hg).trans (stabilizerEquivStabilizer hh) = 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]

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