Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes