smul — Mathlib

English

The action by a group element g fixes the entire product: g • prodXSubSMul G R x = prodXSubSMul G R x.

Русский

Действие элемента группы g фиксирует произведение: g • prodXSubSMul G R x = prodXSubSMul G R x.

LaTeX

$$$g \cdot prodXSubSMul\ G\ R\ x = prodXSubSMul\ G\ R\ x$.$$

Lean4

theorem smul (x : R) (g : G) : g • prodXSubSMul G R x = prodXSubSMul G R x :=
  letI := Classical.decEq R
  Finset.smul_prod'.trans <|
    Fintype.prod_bijective _ (MulAction.bijective g) _ _ fun g' ↦ by
      rw [ofQuotientStabilizer_smul, smul_sub, Polynomial.smul_X, Polynomial.smul_C]

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