Commit 2025-08-07 21:32 deb7399b

View on Github →

feat(Bivariate): aevalAeval and swap (#27636) Add the aeval equivalent to Bivariate.evalEval. This PR also introduces Bivariate.swap, the R-algebra automorphism given by X ↦ Y and Y ↦ X.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

added theorem Polynomial.Bivariate.aevalAeval_swap

added theorem Polynomial.Bivariate.aveal_eq_map_swap

added def Polynomial.Bivariate.swap

added theorem Polynomial.Bivariate.swap_X

added theorem Polynomial.Bivariate.swap_Y

added theorem Polynomial.Bivariate.swap_apply

added theorem Polynomial.Bivariate.swap_monomial_monomial

added theorem Polynomial.coe_aevalAeval_eq_evalEval