Commit 2023-03-13 14:02 59eaf443

View on Github →

feat: Port RingTheory.Polynomial.Tower (#2840) Rename only.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Tower.lean

added theorem Polynomial.aeval_algebraMap_apply

added theorem Polynomial.aeval_algebraMap_eq_zero_iff

added theorem Polynomial.aeval_algebraMap_eq_zero_iff_of_injective

added theorem Polynomial.aeval_map_algebraMap

added theorem Subalgebra.aeval_coe