Commit 2024-12-01 09:59 c8203667

View on Github →

feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff (#17553)

Estimated changes

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

added theorem MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff

Modified Mathlib/Data/Finset/Lattice/Fold.lean

added theorem Finset.comp_sup_eq_sup_comp_of_nonempty