mathlib
0c26348e - feat(data/finsupp/basic): `finsupp.comap_domain` is an `add_monoid_hom` (#13783)

Commit
3 years ago
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. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading