Commit 2022-05-12 08:45 0c26348e
View on Github →feat(data/finsupp/basic): finsupp.comap_domain
is an add_monoid_hom
(#13783)
This is the version of map_domain.add_monoid_hom
for comap_domain
.
I plan to use it for the inclusion of polynomials in Laurent polynomials (#13415).
I also fixed a typo in a doc-string.