ofQuotientStabilizer_smul — Mathlib

English

The quotient stabilizer respects smul: ofQuotientStabilizer(g ⋅ g') = g ⋅ ofQuotientStabilizer(g').

Русский

Стабилизатор-из факторного класса сохраняет умножение: ofQuotientStabilizer(g ⋅ g') = g ⋅ ofQuotientStabilizer(g').

LaTeX

$$$\\operatorname{ofQuotientStabilizer}(\\alpha,x, g \\cdot g') = g \\cdot \\operatorname{ofQuotientStabilizer}(\\alpha,x,g')$$$

Lean4

@[to_additive]
theorem ofQuotientStabilizer_smul (g : α) (g' : α ⧸ MulAction.stabilizer α x) :
    ofQuotientStabilizer α x (g • g') = g • ofQuotientStabilizer α x g' :=
  Quotient.inductionOn' g' fun _ => mul_smul _ _ _

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