stabilizer_mul_eq_left — Mathlib

English

In a setting with a G-action and IsScalarTower G α α, the stabilizer of a•b equals the stabilizer of a: Stab_G(a•b) = Stab_G(a).

Русский

При действии G и IsScalarTower G α α стабилизатор a•b совпадает со стабилизатором a: Stab_G(a•b) = Stab_G(a).

LaTeX

$$\operatorname{Stab}_G(a\cdot b) = \operatorname{Stab}_G(a)$$

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_mul_eq_left [Group α] [IsScalarTower G α α] (a b : α) : stabilizer G (a * b) = stabilizer G a :=
  stabilizer_smul_eq_left a _ <| mul_left_injective _

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