feat(algebra/direct_sum): graded algebras (#8783)
This provides a `direct_sum.galgebra` structure on top of the existing `direct_sum.gmonoid` structure.
This typeclass is used to provide an `algebra R (⨁ i, A i)` instance.
This also renames and improves the stateement of `direct_sum.module.ext` to `direct_sum.linear_map_ext` and adds `direect_sum.ring_hom_ext` and `direct_sum.alg_hom_ext` to match.
