mathlib

94f59d8b - feat(ring_theory/polynomial/homogenous): add a `direct_sum.gcomm_monoid` instance (#6825)

feat(ring_theory/polynomial/homogenous): add a `direct_sum.gcomm_monoid` instance (#6825) This also corrects a stupid typo I made in `direct_sum.comm_ring` which was previously declared a `ring`!