# Divisibility of Separated Polynomials

Lean formalization for `Divisibility of Separated Polynomials`.

The main theorem is `SeparatedPolynomialDifferences.sep_dvd_iff_exists_common_outer`, which verifies the separated divisibility criterion over a field.

It is checked with Lean 4.30.0-rc2 and mathlib v4.30.0-rc2.

```powershell
lake exe cache get SeparatedPolynomialDifferences.lean
lake build
```