homogeneousComponent_C_mul — Mathlib

English

For any r ∈ R and φ ∈ MvPolynomial(σ, R), the degree-n component commutes with multiplication by the constant C r: homogeneousComponent(n)(C r · φ) = C r · homogeneousComponent(n) φ.

Русский

Умножение на константу внутри коэффициентов сохраняет компоненту по степени n: homogeneousComponent(n)(C r · φ) = C r · homogeneousComponent(n) φ.

LaTeX

$$homogeneousComponent(n)(C r · φ) = C r · homogeneousComponent(n) φ$$

Lean4

@[simp]
theorem homogeneousComponent_C_mul (n : ℕ) (r : R) :
    homogeneousComponent n (C r * φ) = C r * homogeneousComponent n φ :=
  weightedHomogeneousComponent_C_mul φ n r

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