Commit 2025-01-23 09:23 403e2d8d

View on Github →

chore(MvPolynomial/Degrees): append _le in lemma names (#20294) The current names are incorrect.

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/CommRing.lean

deleted theorem MvPolynomial.degrees_sub

added theorem MvPolynomial.degrees_sub_le

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

deleted theorem MvPolynomial.degrees_add

added theorem MvPolynomial.degrees_add_le

modified theorem MvPolynomial.degrees_add_of_disjoint

deleted theorem MvPolynomial.degrees_map

added theorem MvPolynomial.degrees_map_le

deleted theorem MvPolynomial.degrees_mul

added theorem MvPolynomial.degrees_mul_le

deleted theorem MvPolynomial.degrees_pow

added theorem MvPolynomial.degrees_pow_le

deleted theorem MvPolynomial.degrees_prod

added theorem MvPolynomial.degrees_prod_le

deleted theorem MvPolynomial.degrees_sum

added theorem MvPolynomial.degrees_sum_le

deleted theorem MvPolynomial.le_degrees_add

added theorem MvPolynomial.le_degrees_add_left

added theorem MvPolynomial.le_degrees_add_right

Modified Mathlib/Algebra/MvPolynomial/Variables.lean

modified theorem MvPolynomial.vars_map

Modified Mathlib/FieldTheory/Finite/Polynomial.lean