Main result
Under the stated hypotheses, f(X)-g(Y) divides
p(X)-q(Y) if and only if p and
q are obtained by composing f and
g with a common outer polynomial.
- Contribution type
- New argument; Lean formalization
- Contribution
- Common-outer-polynomial divisibility criterion for separated polynomial differences, proved through free-module residue expansion and diagonal reduction.
- Mechanism
- free-module residue rectangle and diagonal reduction
- Lean theorem
SeparatedPolynomialDifferences.sep_dvd_iff_exists_common_outer- Lean and mathlib
- Lean 4.30.0-rc2, mathlib v4.30.0-rc2
- Build command
lake build