mathlib3

0d5bed0e - feat(ring_theory/graded_algebra): definitions and basic operations of homogeneous ideal (#10784)

feat(ring_theory/graded_algebra): definitions and basic operations of homogeneous ideal (#10784) This defines homogeneous ideals (`homogeneous_ideal`) of a graded algebra. Co-authored-by: jjaassoonn <jujian.zhang1998@out.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>