abs_poly_dioph — Mathlib

English

The nat-absolute value of a polynomial with integer coefficients, evaluated at a vector, is a Diophantine function.

Русский

Модуль целого многочлена по отношению к вектору является диагофантовой функцией.

LaTeX

$$$$\mathrm{DiophFn}(v \mapsto |p(v)|)$$$$

Lean4

theorem abs_poly_dioph (p : Poly α) : DiophFn fun v => (p v).natAbs :=
  of_no_dummies _ ((p.map some - Poly.proj none) * (p.map some + Poly.proj none)) fun v =>
    (by dsimp; exact Int.natAbs_eq_iff_mul_eq_zero)

Похожие утверждения