Commit 2021-11-02 12:07 da6706d0
View on Github →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.