Commit 2023-04-20 12:31 db5f318e

View on Github →

feat: port Data.MvPolynomial.Funext (#3225)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/MvPolynomial/Basic.lean

added theorem MvPolynomial.eval_eval₂

added theorem MvPolynomial.eval₂_id

Created Mathlib/Data/MvPolynomial/Funext.lean

added theorem MvPolynomial.funext

added theorem MvPolynomial.funext_iff

Created Mathlib/Data/MvPolynomial/Polynomial.lean

added theorem MvPolynomial.eval_polynomial_eval_finSuccEquiv

added theorem MvPolynomial.polynomial_eval_eval₂

Modified Mathlib/Tactic/Conv.lean