Theorem MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff

Modification history

2024-12-01 09:59
Mathlib/Algebra/MvPolynomial/Degrees.lean
feat(Algebra/MvPolynomial/Degrees): degreeOf_mul_X_eq_degreeOf_add_one_iff (#17553)
Added MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iffView on Github →