dvd_dioph — Mathlib

English

If f and g are DiophFn, then the predicate v ↦ f(v) | g(v) is Diophantine.

Русский

Если f и g — диофантовы функции, то предикат v ↦ f(v) | g(v) является диофантовым.

LaTeX

$$$$\\forall \\{\\alpha : Type\\} {f,g:(\\alpha \\to \\mathbb{N})\\to \\mathbb{N},\\;\\mathrm{DiophFn}\\,f \\to \\mathrm{DiophFn}\\,g \\to \\mathrm{Dioph}\\,\\bigl(\\lambda v. f(v) \\mid g(v)\\bigr).$$$$

Lean4

/-- The set of places where one Diophantine function divides another is Diophantine. -/
theorem dvd_dioph : Dioph fun v => f v ∣ g v :=
  dioph_comp ((D∃) 2 <| D&2 D= D&1 D* D&0) [f, g] ⟨df, dg⟩

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