Theorems · Theorem · group theory

AddAction.stabilizerEquivStabilizer_trans

∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {g h k : G} {a b c : α} (hg : b = g +ᵥ a)
  (hh : c = h +ᵥ b) (hk : c = k +ᵥ a),
  k = h + g →
    (AddAction.stabilizerEquivStabilizer hg).trans (AddAction.stabilizerEquivStabilizer hh) =
      AddAction.stabilizerEquivStabilizer hk

Defined in

Mathlib.GroupTheory.GroupAction.Basic

Cited by

0 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Quot.sound

Assumes

AddGroupAddAction