Commit 2024-02-07 14:08 9ac3278b

View on Github →

feat(RingTheory/MvPolynomial): funext for homogeneous polynomials (#10300)

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/Homogeneous.lean

added theorem MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero

added theorem MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card

added theorem MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_coeff_finSuccEquiv_ne_zero_aux

added theorem MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_totalDegree_le_card_aux

added theorem MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous

added theorem MvPolynomial.IsHomogeneous.funext

added theorem MvPolynomial.IsHomogeneous.funext_of_le_card

added theorem MvPolynomial.IsHomogeneous.neg

added theorem MvPolynomial.IsHomogeneous.sub