Commit 2025-12-17 09:29 55d553db

View on Github →

feat(RingTheory/MvPolynomial/MonomialOrder): generalize some IsRegular hypotheses to ∈ nonZeroDivisors (#32780) Similar with #25925, some theorems hypothesizing regular element(s) are generalized to hypothesize non zero-divisors.

Estimated changes

Modified Mathlib/RingTheory/MvPolynomial/Groebner.lean

Modified Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean

added theorem MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors

added theorem MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors

added theorem MonomialOrder.degree_prod_of_mem_nonZeroDivisors

deleted theorem MonomialOrder.degree_smul

added theorem MonomialOrder.degree_smul_of_isRegular

added theorem MonomialOrder.degree_smul_of_mem_nonZeroDivisors

added theorem MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors

added theorem MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors

added theorem MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors