stabilizer_smul_eq_right — Mathlib

English

Under SMul α β, with G' acting on β and SMulCommClass, one has stabilizer of b included in stabilizer of a • b: Stab_G'(b) ≤ Stab_G'(a • b).

Русский

При SMul α β, когда G' действует на β и соблюдается SMulCommClass, выполняется включение стабилизатора b в стабилизатор a • b.

LaTeX

$$\operatorname{Stab}_{G'}(b) \le \operatorname{Stab}_{G'}(a \cdot b)$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_smul_eq_right {α} [Group α] [MulAction α β] [SMulCommClass G α β] (a : α) (b : β) :
    stabilizer G (a • b) = stabilizer G b :=
  (le_stabilizer_smul_right _ _).antisymm' <| (le_stabilizer_smul_right a⁻¹ _).trans_eq <| by rw [inv_smul_smul]

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