mathlib

da6706d0 - feat(data/mv_polynomial/basic): lemmas about map (#10092)

feat(data/mv_polynomial/basic): lemmas about map (#10092) This adds `map_alg_hom`, which fills the gap between `map` and `map_alg_equiv`. The only new proof here is `map_surjective`; everything else is just a reworked existing proof.