Theorems · Definition · number theory

Dioph

{α : Type u} → Set (α → ℕ) → Prop

A set S ⊆ ℕ^α is Diophantine if there exists a polynomial on α ⊕ β such that v ∈ S iff there exists t : ℕ^β with p (v, t) = 0.

Defined in

Mathlib.NumberTheory.Dioph

Cited by

30 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms