English
The submodule generated by products P_m · P_n of weighted homogeneous polynomials of degrees m and n is contained in the submodule of weighted homogeneous polynomials of degree m+n.
Русский
Подмодуль, порождённый произведениями P_m · P_n взвешенно однородных многочленов степеней m и n, содержится в подмодуле взвешенно однородных многочленов степени m+n.
LaTeX
$$weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤ weightedHomogeneousSubmodule R w (m+n)$$
Lean4
/-- The submodule generated by products `Pm * Pn` of weighted homogeneous polynomials of degrees `m`
and `n` is contained in the submodule of weighted homogeneous polynomials of degree `m + n`. -/
theorem weightedHomogeneousSubmodule_mul (w : σ → M) (m n : M) :
weightedHomogeneousSubmodule R w m * weightedHomogeneousSubmodule R w n ≤
weightedHomogeneousSubmodule R w (m + n) :=
by
classical
rw [Submodule.mul_le]
intro φ hφ ψ hψ c hc
rw [coeff_mul] at hc
obtain ⟨⟨d, e⟩, hde, H⟩ := Finset.exists_ne_zero_of_sum_ne_zero hc
have aux : coeff d φ ≠ 0 ∧ coeff e ψ ≠ 0 := by
contrapose! H
by_cases h : coeff d φ = 0 <;> simp_all only [Ne, not_false_iff, zero_mul, mul_zero]
rw [← mem_antidiagonal.mp hde, ← hφ aux.1, ← hψ aux.2, map_add]
