mathlib

efbbb767 - feat(ring_theory/graded_algebra): `homogeneous_element` (#10118)

feat(ring_theory/graded_algebra): `homogeneous_element` (#10118) This pr is about what `homogeneous_element` of graded ring is. We need this definition to make the definition of homogeneous ideal more natural, i.e. we can say that a homogeneous ideal is just an ideal spanned by homogeneous elements. Co-authored-by: jjaassoonn <jujian.zhang1998@out.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>