[Merged by Bors] - feat(Polynomial/AlgebraMap): add `mapAlgHom`#14814

Closed

quangvdao wants to merge 5 commits intomasterfrom Polynomial.mapAlgHom

Commits on Jul 13, 2024

Added mapAlgHom as the algebra version of mapRingHom, and supporting theorems
quangvdao
committed

Commits on Jul 15, 2024

golf
quangvdao
committed

Commits on Jul 16, 2024

Commits on Jul 17, 2024

added simp theorems for mapAlgEquiv
quangvdao
committed