Commit 2025-12-01 17:55 b0f11fe7

View on Github →

feat: divisibility lemmas for multivariate polynomials (#32226) Prove several divisibility lemmas for multivariate polynomials, of the form: if $$p$$ divides $$X ^ n * q$$, then there exists $$m\leq n$$ and $$p'$$ dividing $$q$$ such that $$p = X^m * p'$$. They come from a particular case that was proven in #31161 .

Estimated changes