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.

Estimated changes

Modified src/algebra/direct_sum_graded.lean

added def direct_sum.lift_ring_hom

added theorem direct_sum.ring_hom_ext'

added def direct_sum.to_semiring

added theorem direct_sum.to_semiring_coe_add_monoid_hom

added theorem direct_sum.to_semiring_of