Commit 2021-12-13 15:33 efbbb767

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.