sum_homogeneousComponent — Mathlib

English

The polynomial φ is the finite sum of its homogeneous components: ∑_{i=0}^{φ.totalDegree} homogeneousComponent(i) φ = φ.

Русский

Многочлен φ равен конечной сумме своих однородных компонент: ∑_{i=0}^{deg(φ)} homogeneousComponent(i) φ = φ.

LaTeX

$$∑_{i=0}^{φ.totalDegree} homogeneousComponent(i) φ = φ$$

Lean4

theorem sum_homogeneousComponent : (∑ i ∈ range (φ.totalDegree + 1), homogeneousComponent i φ) = φ :=
  by
  ext1 d
  suffices φ.totalDegree < d.support.sum d → 0 = coeff d φ by simpa [coeff_sum, coeff_homogeneousComponent]
  exact fun h => (coeff_eq_zero_of_totalDegree_lt h).symm

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