Commit 2022-06-29 22:22 a2a8c9be

refactor(ring_theory/graded_algebra): use add_submonoid_class to generalize to graded rings (#14583) Now that we have add_submonoid_class, we don't need to consider only families of submodules. For convenience, this keeps around graded_algebra as an alias for graded_ring over a family of submodules, as this can help with elaboration here and there. This renames:

• graded_algebra to graded_ring
• graded_algebra.proj_zero_ring_hom to graded_ring.proj_zero_ring_hom adds:
• direct_sum.decompose_ring_equiv
• graded_ring.proj
• graded_algebra (as an alias for a suitable graded_ring and removes:
• graded_algebra.is_internal, which was just an alias anyway.