Commit 2025-01-31 20:52 b8068ea5

feat: Lemmas for some monomial orders (#16177) This is a PR of technical lemmas relative to monomial orders and polynomials that were taken out of the formalization of Alon's Combinatorial Nullstellensatz which now belongs to #20495

• degree of a product for the deglex monomial order, multiplicativity of the leading coefficients
• degree (for a monomial order) of monomials
• the leading coefficient (for a monomial order) of a nonzero polynomial is nonzero.