feat(algebra/graded_monoid): dependent products (#10674)
This introduces `list.dprod`, which takes the (possibly non-commutative) product of a list of graded elements of type `A i`. This definition primarily exist to allow `graded_monoid.mk` and `direct_sum.of` to be pulled outside a product, such as in the new `graded_monoid.mk_list_dprod` and `direct_sum.of_list_dprod` lemmas added in this PR.
