feat(algebra/direct_sum_graded): endow direct_sum with a ring struc…

…ture (#6053)

To quote the module docstring

> This module provides a set of heterogenous typeclasses for defining a multiplicative structure
> over `⨁ i, A i` such that `(*) : A i → A j → A (i + j)`; that is to say, `A` forms an
> additively-graded ring. The typeclasses are:
> 
> * `direct_sum.ghas_one A`
> * `direct_sum.ghas_mul A`
> * `direct_sum.gmonoid A`
> * `direct_sum.gcomm_monoid A`
> 
> Respectively, these imbue the direct sum `⨁ i, A i` with:
> 
> * `has_one`
> * `mul_zero_class`, `distrib`
> * `semiring`, `ring`
> * `comm_semiring`, `comm_ring`
>
> Additionally, this module provides helper functions to construct `gmonoid` and `gcomm_monoid`
> instances for:
> 
> * `A : ι → submonoid S`: `direct_sum.ghas_one.of_submonoids`, `direct_sum.ghas_mul.of_submonoids`,
>   `direct_sum.gmonoid.of_submonoids`, `direct_sum.gcomm_monoid.of_submonoids`
> * `A : ι → submonoid S`: `direct_sum.ghas_one.of_subgroups`, `direct_sum.ghas_mul.of_subgroups`,
>   `direct_sum.gmonoid.of_subgroups`, `direct_sum.gcomm_monoid.of_subgroups`
> 
> If the `A i` are disjoint, these provide a gradation of `⨆ i, A i`, and the mapping
> `⨁ i, A i →+ ⨆ i, A i` can be obtained as
> `direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)`.