mathlib

d199eb99 - feat(ring_theory/graded_algebra/homogeneous_ideal): refactor `homogeneous_ideal` as a structure extending ideals (#12673)

feat(ring_theory/graded_algebra/homogeneous_ideal): refactor `homogeneous_ideal` as a structure extending ideals (#12673) We refactored `homogeneous_ideal` as a structure extending ideals so that we can define a `set_like (homogeneous_ideal \McA) A` instance.