mathlib3

a2a8c9be - refactor(ring_theory/graded_algebra): use `add_submonoid_class` to generalize to graded rings (#14583)

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. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>