English
The product of two weighted homogeneous power series with weights p and q is weighted homogeneous of weight p+q.
Русский
Произведение двух взвешенно однородных рядов весов p и q является взвешенно однородным по весу p+q.
LaTeX
$$$ \text{IsWeightedHomogeneous w p} \ f \Rightarrow \text{IsWeightedHomogeneous w q} \ g \Rightarrow \text{IsWeightedHomogeneous w (p+q)} (f \cdot g) $$$
Lean4
protected theorem mul {f g : MvPowerSeries σ R} {p q : ℕ} (hf : f.IsWeightedHomogeneous w p)
(hg : g.IsWeightedHomogeneous w q) : (f * g).IsWeightedHomogeneous w (p + q) := fun {d} ↦ by
classical
rw [not_imp_comm]
intro hd
rw [coeff_mul]
apply Finset.sum_eq_zero
intro x hx
rw [Finset.mem_antidiagonal] at hx
suffices weight w x.1 ≠ p ∨ weight w x.2 ≠ q by
rcases this with hp | hq
· rw [hf.coeff_eq_zero hp, zero_mul]
· rw [hg.coeff_eq_zero hq, mul_zero]
rw [← not_and_or]
rintro ⟨hp, hq⟩
apply hd
rw [← hx, map_add, hp, hq]
