Commit 2023-08-10 22:19 057299dc

View on Github →

feat: Add a DecidableEq instance for Polynomial (#5942) Add a DecidableEq instance for Polynomial (in the presence of DecidableEq for coefficients). This instance is the companion of an analogue instance for MvPolynomial, and it allows to use if… then… else for Polynomial without having to open Classical. This also makes Polynomial.instNormalizationMonoid computable, by defining it in terms of this new instance.

Estimated changes

Modified Mathlib/Data/Polynomial/Basic.lean

Modified Mathlib/Data/Polynomial/Degree/CardPowDegree.lean

modified theorem Polynomial.cardPowDegree_zero

Modified Mathlib/Data/Polynomial/FieldDivision.lean

modified theorem Polynomial.coe_normUnit_of_ne_zero

modified theorem Polynomial.degree_normalize

modified theorem Polynomial.eval_gcd_eq_zero

modified theorem Polynomial.eval₂_gcd_eq_zero

modified theorem Polynomial.gcd_map

modified theorem Polynomial.isRoot_gcd_iff_isRoot_left_right

modified theorem Polynomial.monic_normalize

modified theorem Polynomial.normalize_monic

modified theorem Polynomial.root_gcd_iff_root_left_right

modified theorem Polynomial.root_left_of_root_gcd

modified theorem Polynomial.root_right_of_root_gcd