Commit 2024-02-03 01:01 0e978d6f

View on Github →

chore: misc lemmas about polynomials (#10193)

Estimated changes

Modified Mathlib/Data/MvPolynomial/Rename.lean

added theorem MvPolynomial.coeff_rename_embDomain

added theorem MvPolynomial.eval_rename

Modified Mathlib/Data/MvPolynomial/Variables.lean

added theorem MvPolynomial.degreeOf_le_iff

added theorem MvPolynomial.degreeOf_le_totalDegree

Modified Mathlib/Data/Polynomial/RingDivision.lean

added theorem Polynomial.exists_eval_ne_zero_of_natDegree_lt_card

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.IsHomogeneous.rename_isHomogeneous