Commit 2024-07-17 17:08 59122192

View on Github →

feat(Polynomial/AlgebraMap): add mapAlgHom (#14814) Add Polynomial.mapAlgHom as an algebra homomorphism between two polynomial rings, extending Polynomial.mapRingHom. Provide supporting theorems for mapAlgHom. Moved Polynomial.eval₂AlgHom' to earlier in AlgebraMap.lean , so that I can provide a theorem linking mapAlgHom and eval₂AlgHom', without having to put mapAlgHom stuff after aeval.

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added theorem Polynomial.coe_mapAlgEquiv

added theorem Polynomial.coe_mapAlgHom

added def Polynomial.mapAlgEquiv

added theorem Polynomial.mapAlgEquiv_coe_ringHom

added theorem Polynomial.mapAlgEquiv_comp

added theorem Polynomial.mapAlgEquiv_id

added def Polynomial.mapAlgHom

added theorem Polynomial.mapAlgHom_coe_ringHom

added theorem Polynomial.mapAlgHom_comp

added theorem Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom

added theorem Polynomial.mapAlgHom_id