mathlib3

a07cf6bd - feat(ring_theory/polynomial/homogeneous) : add lemma `homogeneous_component_homogeneous_polynomial` (#10113)

feat(ring_theory/polynomial/homogeneous) : add lemma `homogeneous_component_homogeneous_polynomial` (#10113) add the following lemma ```lean lemma homogeneous_component_homogeneous_polynomial (m n : ℕ) (p : mv_polynomial σ R) (h : p ∈ homogeneous_submodule σ R n) : homogeneous_component m p = if m = n then p else 0 ``` Co-authored-by: jjaassoonn <jujian.zhang1998@out.com>