Commit 2021-08-30 13:16 98466d29

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.