Theorem MvPolynomial.totalDegree_sub_C_le

Modification history

2023-12-04 20:27
Mathlib/Data/MvPolynomial/CommRing.lean
feat: add a few lemmas about MvPolynomial.totalDegree (#8815) …
Added MvPolynomial.totalDegree_sub_C_leView on Github →