stabilizerEquivStabilizer_compTriple

English

For additive groups, the stabilizers compose to give a triple of commuting stabilizer equivalences.

Русский

Для аддитивных групп композиция стабилизаторов образует тройку совместимых эквивалентностей стабилизаторов.

LaTeX

$$$\text{AddAction.stabilizerEquivStabilizer\_compTriple}$$$

Lean4

theorem _root_.AddAction.stabilizerEquivStabilizer_compTriple {G : Type*} [AddGroup G] {α : Type*} [AddAction G α]
    {g h k : G} {a b c : α} {hg : b = g +ᵥ a} {hh : c = h +ᵥ b} {hk : c = k +ᵥ a} (H : k = h + g) :
    CompTriple (AddAction.stabilizerEquivStabilizer hg) (AddAction.stabilizerEquivStabilizer hh)
      (AddAction.stabilizerEquivStabilizer hk)
    where
  comp_eq := by
    ext
    simp [AddAction.stabilizerEquivStabilizer, H, AddAut.conj, ← add_assoc]

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