English
A polynomial is the sum of its weighted homogeneous components: φ = sum_m weightedHomogeneousComponent w m φ.
Русский
Полином является суммой своих взвешенных однородных компонент: φ = ∑_m weightedHomogeneousComponent w m φ.
LaTeX
$$$\\varphi = \\sum_{m} weightedHomogeneousComponent w m \\varphi$$$
Lean4
/-- Every polynomial is the sum of its weighted homogeneous components. -/
theorem sum_weightedHomogeneousComponent : (finsum fun m => weightedHomogeneousComponent w m φ) = φ := by
classical
rw [finsum_eq_sum _ (weightedHomogeneousComponent_finsupp φ)]
ext1 d
simp only [coeff_sum, coeff_weightedHomogeneousComponent]
rw [Finset.sum_eq_single (weight w d)]
· rw [if_pos rfl]
· intro m _ hm'
rw [if_neg hm'.symm]
· intro hm
rw [if_pos rfl]
simp only [Finite.mem_toFinset, mem_support, Ne, Classical.not_not] at hm
have := coeff_weightedHomogeneousComponent (w := w) (weight w d) φ d
rw [hm, if_pos rfl, coeff_zero] at this
exact this.symm
