Commit 2026-03-03 23:24 c5a9b272

View on Github →

feat(RingTheory/MvPolynomial): add eval results (#35803) Co-authored by: @AntoineChambert-Loir.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Eval.lean

added theorem MvPolynomial.aeval_range

added theorem MvPolynomial.coe_eval₂AlgHom

added def MvPolynomial.eval₂AlgHom

added theorem MvPolynomial.eval₂AlgHom_X

added theorem MvPolynomial.eval₂AlgHom_apply

added theorem MvPolynomial.eval₂Hom_smul

added theorem MvPolynomial.eval₂_X_pow

added theorem MvPolynomial.eval₂_mul_eq_zero_of_left

added theorem MvPolynomial.eval₂_mul_eq_zero_of_right

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

deleted def Polynomial.eval₂AlgHom'

added def Polynomial.eval₂AlgHom

deleted theorem Polynomial.mapAlgHom_eq_eval₂AlgHom'_CAlgHom

added theorem Polynomial.mapAlgHom_eq_eval₂AlgHom_CAlgHom

Modified Mathlib/LinearAlgebra/Semisimple.lean

Modified Mathlib/RingTheory/MatrixPolynomialAlgebra.lean

Modified Mathlib/RingTheory/MvPolynomial/Ideal.lean

added theorem MvPolynomial.mk_eq_eval₂

added theorem MvPolynomial.mkₐ_eq_aeval