mathlib3

a8d285cc - feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure (#6053)

feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure (#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)`.