stabilizer_mul_eq_right — Mathlib

English

In a setting with Group α, MulAction α β and SMulCommClass G α β, the stabilizer of a•b equals the stabilizer of b: Stab_G(a•b) = Stab_G(b).

Русский

При Group α, MulAction α β и SMulCommClass G α β получаем Stab_G(a•b) = Stab_G(b).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem stabilizer_mul_eq_right [Group α] [SMulCommClass G α α] (a b : α) : stabilizer G (a * b) = stabilizer G b :=
  stabilizer_smul_eq_right a _

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