Commit 2024-08-23 04:06 1699b550

View on Github →

feat(Algebra/Polynomial/Bivariate): add lemmas for bivariate polynomials (#14579)

Estimated changes

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

modified theorem Polynomial.evalEvalRingHom_eq

added theorem Polynomial.evalEval_CC

added theorem Polynomial.evalEval_add

added theorem Polynomial.evalEval_dvd

added theorem Polynomial.evalEval_finset_sum

added theorem Polynomial.evalEval_intCast

added theorem Polynomial.evalEval_list_prod

added theorem Polynomial.evalEval_mul

added theorem Polynomial.evalEval_multiset_prod

added theorem Polynomial.evalEval_natCast

added theorem Polynomial.evalEval_neg

added theorem Polynomial.evalEval_one

added theorem Polynomial.evalEval_pow

added theorem Polynomial.evalEval_prod

added theorem Polynomial.evalEval_smul

added theorem Polynomial.evalEval_sub

added theorem Polynomial.evalEval_sum

added theorem Polynomial.evalEval_surjective

added theorem Polynomial.evalEval_zero

modified theorem Polynomial.eval₂_evalRingHom