Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-18 11:37 ae72826a

View on Github →

feat(data/mv_polynomial): define comap (#4161) More from the Witt vector branch. Co-authored by: Johan Commelin johan@commelin.net

Estimated changes

Modified src/algebra/category/CommRing/adjunctions.lean

Created src/data/mv_polynomial/comap.lean

added theorem mv_polynomial.comap_apply

added theorem mv_polynomial.comap_comp

added theorem mv_polynomial.comap_comp_apply

added theorem mv_polynomial.comap_eq_id_of_eq_id

added theorem mv_polynomial.comap_equiv_coe

added theorem mv_polynomial.comap_equiv_symm_coe

added theorem mv_polynomial.comap_id

added theorem mv_polynomial.comap_id_apply

added theorem mv_polynomial.comap_rename

Modified src/data/mv_polynomial/rename.lean

modified def mv_polynomial.rename