Commit 2023-03-15 10:05 fc4a489c

View on Github →

feat: port RingTheory.MvPolynomial.Tower (#2897)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/MvPolynomial/Tower.lean

added theorem MvPolynomial.aeval_algebraMap_apply

added theorem MvPolynomial.aeval_algebraMap_eq_zero_iff

added theorem MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective

added theorem MvPolynomial.aeval_map_algebraMap

added theorem Subalgebra.mvPolynomial_aeval_coe