# Commit 2021-05-05 18:50 51bc1ca4

View on Github →feat(algebra/direct_sum_graded): add direct_sum.to_semiring (#7380)
This provides a convenient way to construct ring_homs out of `direct_sum`

, and is a stronger version of `direct_sum.to_add_monoid`

which applies in the presence of a `direct_sum.gmonoid`

typeclass.
The new `direct_sum.lift_ring_hom`

can be thought of as a universal property akin to `finsupp.lift_add_hom`

.