Commit 2025-03-20 05:49 11034907

View on Github →

feat(RingTheory): add Polynomial.toMvPolynomial (#22922)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

added theorem MvPolynomial.aeval_comp_toMvPolynomial

added theorem MvPolynomial.aeval_toMvPolynomial

added theorem MvPolynomial.eval_comp_toMvPolynomial

added theorem MvPolynomial.eval_toMvPolynomial

added theorem MvPolynomial.rename_comp_toMvPolynomial

added theorem MvPolynomial.rename_toMvPolynomial

added theorem Polynomial.toMvPolynomial_C

added theorem Polynomial.toMvPolynomial_X

added theorem Polynomial.toMvPolynomial_eq_rename_comp

added theorem Polynomial.toMvPolynomial_injective