mathlib

976f5106 - feat(ring_theory/graded_algebra/basic): add lemma `proj_homogeneous_mul` (#15264)

feat(ring_theory/graded_algebra/basic): add lemma `proj_homogeneous_mul` (#15264) added a lemma stating that $(ab)_{i+j}=ab_j$ for homogeneous $a$ with degree $I$ Co-authored-by: Eric Wieser @eric-wieser