coeff — Mathlib

English

The coefficient after applying group action equals the original coefficient: g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n.

Русский

После применения действия группы коэффициент остаётся неизменным: g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n.

LaTeX

$$$g \cdot (prodXSubSMul\ G\ R\ x).\text{coeff } n = (prodXSubSMul\ G\ R\ x).\text{coeff } n$.$$

Lean4

theorem coeff (x : R) (g : G) (n : ℕ) : g • (prodXSubSMul G R x).coeff n = (prodXSubSMul G R x).coeff n := by
  rw [← Polynomial.coeff_smul, prodXSubSMul.smul]

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