Commit 2026-03-04 12:02 816802b4

View on Github →

feat(Algebra/Polynomial): add aevalEquiv and its bivariate version (#35283)

Estimated changes

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

added def Polynomial.aevalEquiv

added theorem Polynomial.aevalEquiv_apply

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

added def Polynomial.aevalAevalEquiv

added theorem Polynomial.aevalAevalEquiv_apply

added theorem Polynomial.aevalAeval_C

added theorem Polynomial.aevalAeval_X

added theorem Polynomial.aevalAeval_Y

Modified Mathlib/FieldTheory/RatFunc/Luroth.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

modified theorem AdjoinRoot.liftHom_mk