mathlib documentation

number_theory.dioph

source
theorem int.eq_nat_abs_iff_mul (x : ℤ) (n : ℕ) :
x.nat_abs = n ↔ (x - ↑n) * (x + ↑n) = 0

source
def vector3 (α : Type u) (n : ℕ) :
Type u

Alternate definition of vector based on fin2.

Equations
source
def vector3.nil {α : Type u_1} :
vector3 α 0

The empty vector

source
def vector3.cons {α : Type u_1} {n : ℕ} (a : α) (v : vector3 α n) :
vector3 α n.succ

The vector cons operation

Equations
source
@[simp]
theorem vector3.cons_fz {α : Type u_1} {n : ℕ} (a : α) (v : vector3 α n) :
(a :: v) fin2.fz = a

source
@[simp]
theorem vector3.cons_fs {α : Type u_1} {n : ℕ} (a : α) (v : vector3 α n) (i : fin2 n) :
(a :: v) i.fs = v i

source
def vector3.nth {α : Type u_1} {n : ℕ} (i : fin2 n) (v : vector3 α n) :
α

Get the ith element of a vector

Equations
source
def vector3.of_fn {α : Type u_1} {n : ℕ} (f : fin2 n → α) :
vector3 α n

Construct a vector from a function on fin2.

Equations
source
def vector3.head {α : Type u_1} {n : ℕ} (v : vector3 α n.succ) :
α

Get the head of a nonempty vector.

Equations
source
def vector3.tail {α : Type u_1} {n : ℕ} (v : vector3 α n.succ) :
vector3 α n

Get the tail of a nonempty vector.

Equations
source
theorem vector3.eq_nil {α : Type u_1} (v : vector3 α 0) :
v = vector3.nil

source
theorem vector3.cons_head_tail {α : Type u_1} {n : ℕ} (v : vector3 α n.succ) :
v.head :: v.tail = v

source
def vector3.nil_elim {α : Type u_1} {C : vector3 α 0 → Sort u} (H : C vector3.nil) (v : vector3 α 0) :
C v

Equations
source
def vector3.cons_elim {α : Type u_1} {n : ℕ} {C : vector3 α n.succ → Sort u} (H : Π (a : α) (t : vector3 α n), C (a :: t)) (v : vector3 α n.succ) :
C v

Equations
source
@[simp]
theorem vector3.cons_elim_cons {α : Type u_1} {n : ℕ} {C : vector3 α n.succ → Sort u_2} {H : Π (a : α) (t : vector3 α n), C (a :: t)} {a : α} {t : vector3 α n} :
vector3.cons_elim H (a :: t) = H a t

source
def vector3.rec_on {α : Type u_1} {C : Π {n : ℕ}, vector3 α n → Sort u} {n : ℕ} (v : vector3 α n) (H0 : C vector3.nil) (Hs : Π {n : ℕ} (a : α) (w : vector3 α n), C w → C (a :: w)) :
C v

Equations
source
@[simp]
theorem vector3.rec_on_nil {α : Type u_1} {C : Π {n : ℕ}, vector3 α n → Sort u_2} {H0 : C vector3.nil} {Hs : Π {n : ℕ} (a : α) (w : vector3 α n), C w → C (a :: w)} :
vector3.nil.rec_on H0 Hs = H0

source
@[simp]
theorem vector3.rec_on_cons {α : Type u_1} {C : Π {n : ℕ}, vector3 α n → Sort u_2} {H0 : C vector3.nil} {Hs : Π {n : ℕ} (a : α) (w : vector3 α n), C w → C (a :: w)} {n : ℕ} {a : α} {v : vector3 α n} :
(a :: v).rec_on H0 Hs = Hs a v (v.rec_on H0 Hs)

source
def vector3.append {α : Type u_1} {m : ℕ} (v : vector3 α m) {n : ℕ} (w : vector3 α n) :
vector3 α (n + m)

Append two vectors

Equations
source
@[simp]
theorem vector3.append_nil {α : Type u_1} {n : ℕ} (w : vector3 α n) :
vector3.nil.append w = w

source
@[simp]
theorem vector3.append_cons {α : Type u_1} (a : α) {m : ℕ} (v : vector3 α m) {n : ℕ} (w : vector3 α n) :
(a :: v).append w = a :: v.append w

source
@[simp]
theorem vector3.append_left {α : Type u_1} {m : ℕ} (i : fin2 m) (v : vector3 α m) {n : ℕ} (w : vector3 α n) :
v.append w (fin2.left n i) = v i

source
@[simp]
theorem vector3.append_add {α : Type u_1} {m : ℕ} (v : vector3 α m) {n : ℕ} (w : vector3 α n) (i : fin2 n) :
v.append w (i.add m) = w i

source
def vector3.insert {α : Type u_1} (a : α) {n : ℕ} (v : vector3 α n) (i : fin2 n.succ) :
vector3 α n.succ

Insert a into v at index i.

Equations
source
@[simp]
theorem vector3.insert_fz {α : Type u_1} (a : α) {n : ℕ} (v : vector3 α n) :
vector3.insert a v fin2.fz = a :: v

source
@[simp]
theorem vector3.insert_fs {α : Type u_1} (a : α) {n : ℕ} (b : α) (v : vector3 α n) (i : fin2 n.succ) :
vector3.insert a (b :: v) i.fs = b :: vector3.insert a v i

source
theorem vector3.append_insert {α : Type u_1} (a : α) {k : ℕ} (t : vector3 α k) {n : ℕ} (v : vector3 α n) (i : fin2 n.succ) (e : n.succ + k = (n + k).succ) :
vector3.insert a (t.append v) (e.rec_on (i.add k)) = e.rec_on (t.append (vector3.insert a v i))

source
def vector_ex {α : Type u_1} (k : ℕ) (a : vector3 α k → Prop) :
Prop

"Curried" exists, i.e. ∃ x1 ... xn, f [x1, ..., xn]

Equations
source
def vector_all {α : Type u_1} (k : ℕ) (a : vector3 α k → Prop) :
Prop

"Curried" forall, i.e. ∀ x1 ... xn, f [x1, ..., xn]

Equations
source
theorem exists_vector_zero {α : Type u_1} (f : vector3 α 0 → Prop) :
Exists f ↔ f vector3.nil

source
theorem exists_vector_succ {α : Type u_1} {n : ℕ} (f : vector3 α n.succ → Prop) :
Exists f ↔ ∃ (x : α) (v : vector3 α n), f (x :: v)

source
theorem vector_ex_iff_exists {α : Type u_1} {n : ℕ} (f : vector3 α n → Prop) :
vector_ex n f ↔ Exists f

source
theorem vector_all_iff_forall {α : Type u_1} {n : ℕ} (f : vector3 α n → Prop) :
vector_all n f ↔ ∀ (v : vector3 α n), f v

source
def vector_allp {α : Type u_1} (p : α → Prop) {n : ℕ} (v : vector3 α n) :
Prop

vector_allp p v is equivalent to ∀ i, p (v i), but unfolds directly to a conjunction, i.e. vector_allp p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations
source
@[simp]
theorem vector_allp_nil {α : Type u_1} (p : α → Prop) :
vector_allp p vector3.nil = true

source
@[simp]
theorem vector_allp_singleton {α : Type u_1} (p : α → Prop) (x : α) :
vector_allp p (x :: vector3.nil) = p x

source
@[simp]
theorem vector_allp_cons {α : Type u_1} (p : α → Prop) {n : ℕ} (x : α) (v : vector3 α n) :
vector_allp p (x :: v) ↔ p x ∧ vector_allp p v

source
theorem vector_allp_iff_forall {α : Type u_1} (p : α → Prop) {n : ℕ} (v : vector3 α n) :
vector_allp p v ↔ ∀ (i : fin2 n), p (v i)

source
theorem vector_allp.imp {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p x → q x) {n : ℕ} {v : vector3 α n} (al : vector_allp p v) :
vector_allp q v

source
@[simp]
def list_all {α : Type u_1} (p : α → Prop) (a : list α) :
Prop

list_all p l is equivalent to ∀ a ∈ l, p a, but unfolds directly to a conjunction, i.e. list_all p [0, 1, 2] = p 0 ∧ p 1 ∧ p 2.

Equations
source
@[simp]
theorem list_all_cons {α : Type u_1} (p : α → Prop) (x : α) (l : list α) :
list_all p (x :: l) ↔ p x ∧ list_all p l

source
theorem list_all_iff_forall {α : Type u_1} (p : α → Prop) (l : list α) :
list_all p l ↔ ∀ (x : α), x ∈ l → p x

source
theorem list_all.imp {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p x → q x) {l : list α} (a : list_all p l) :
list_all q l

source
@[simp]
theorem list_all_map {α : Type u_1} {β : Type u_2} {p : β → Prop} (f : α → β) {l : list α} :
list_all p (list.map f l) ↔ list_all (p ∘ f) l

source
theorem list_all_congr {α : Type u_1} {p q : α → Prop} (h : ∀ (x : α), p x ↔ q x) {l : list α} :
list_all p l ↔ list_all q l

source
@[instance]
def decidable_list_all {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : list α) :
decidable (list_all p l)

Equations
source
inductive is_poly {α : Sort u_1} (a : (α → ℕ) → ℤ) :
Prop

A predicate asserting that a function is a multivariate integer polynomial. (We are being a bit lazy here by allowing many representations for multiplication, rather than only allowing monomials and addition, but the definition is equivalent and this is easier to use.)

source
def poly (α : Type u) :
Type u

The type of multivariate integer polynomials

Equations
source
@[instance]
def poly.has_coe_to_fun {α : Type u} :
has_coe_to_fun (poly α)

Equations
source
theorem poly.isp {α : Type u} (f : poly α) :
is_poly ⇑f

The underlying function of a poly is a polynomial

source
theorem poly.ext {α : Type u} {f g : poly α} (e : ∀ (x : α → ℕ), ⇑f x = ⇑g x) :
f = g

Extensionality for poly α

source
def poly.subst {α : Type u} (f : poly α) (g : (α → ℕ) → ℤ) (e : ∀ (x : α → ℕ), ⇑f x = g x) :
poly α

Construct a poly given an extensionally equivalent poly.

Equations
source
@[simp]
theorem poly.subst_eval {α : Type u} (f : poly α) (g : (α → ℕ) → ℤ) (e : ∀ (x : α → ℕ), ⇑f x = g x) (x : α → ℕ) :
⇑(f.subst g e) x = g x

source
def poly.proj {α : Type u} (i : α) :
poly α

The ith projection function, x_i.

Equations
source
@[simp]
theorem poly.proj_eval {α : Type u} (i : α) (x : α → ℕ) :
⇑(poly.proj i) x = ↑(x i)

source
def poly.const {α : Type u} (n : ℤ) :
poly α

The constant function with value n : ℤ.

Equations
source
@[simp]
theorem poly.const_eval {α : Type u} (n : ℤ) (x : α → ℕ) :
⇑(poly.const n) x = n

source
def poly.zero {α : Type u} :
poly α

The zero polynomial

Equations
source
@[instance]
def poly.has_zero {α : Type u} :
has_zero (poly α)

Equations
source
@[simp]
theorem poly.zero_eval {α : Type u} (x : α → ℕ) :
⇑0 x = 0

source
def poly.one {α : Type u} :
poly α

The zero polynomial

Equations
source
@[instance]
def poly.has_one {α : Type u} :
has_one (poly α)

Equations
source
@[simp]
theorem poly.one_eval {α : Type u} (x : α → ℕ) :
⇑1 x = 1

source
def poly.sub {α : Type u} (a a_1 : poly α) :
poly α

Subtraction of polynomials

Equations
source
@[instance]
def poly.has_sub {α : Type u} :
has_sub (poly α)

Equations
source
@[simp]
theorem poly.sub_eval {α : Type u} (f g : poly α) (x : α → ℕ) :
⇑(f - g) x = ⇑f x - ⇑g x

source
def poly.neg {α : Type u} (f : poly α) :
poly α

Negation of a polynomial

Equations
source
@[instance]
def poly.has_neg {α : Type u} :
has_neg (poly α)

Equations
source
@[simp]
theorem poly.neg_eval {α : Type u} (f : poly α) (x : α → ℕ) :
(⇑-f) x = -⇑f x

source
def poly.add {α : Type u} (a a_1 : poly α) :
poly α

Addition of polynomials

Equations
source
@[instance]
def poly.has_add {α : Type u} :
has_add (poly α)

Equations
source
@[simp]
theorem poly.add_eval {α : Type u} (f g : poly α) (x : α → ℕ) :
⇑(f + g) x = ⇑f x + ⇑g x

source
def poly.mul {α : Type u} (a a_1 : poly α) :
poly α

Multiplication of polynomials

Equations
source
@[instance]
def poly.has_mul {α : Type u} :
has_mul (poly α)

Equations
source
@[simp]
theorem poly.mul_eval {α : Type u} (f g : poly α) (x : α → ℕ) :
(⇑f * g) x = (⇑f x) * ⇑g x

source
@[instance]
def poly.comm_ring {α : Type u} :
comm_ring (poly α)

Equations
source
theorem poly.induction {α : Type u} {C : poly α → Prop} (H1 : ∀ (i : α), C (poly.proj i)) (H2 : ∀ (n : ℤ), C (poly.const n)) (H3 : ∀ (f g : poly α), C f → C g → C (f - g)) (H4 : ∀ (f g : poly α), C f → C g → C (f * g)) (f : poly α) :
C f

source
def poly.sumsq {α : Type u} (a : list (poly α)) :
poly α

The sum of squares of a list of polynomials. This is relevant for Diophantine equations, because it means that a list of equations can be encoded as a single equation: x = 0 ∧ y = 0 ∧ z = 0 is equivalent to x^2 + y^2 + z^2 = 0.

Equations
source
theorem poly.sumsq_nonneg {α : Type u} (x : α → ℕ) (l : list (poly α)) :
0 ≤ ⇑(poly.sumsq l) x

source
theorem poly.sumsq_eq_zero {α : Type u} (x : α → ℕ) (l : list (poly α)) :
⇑(poly.sumsq l) x = 0 ↔ list_all (λ (a : poly α), ⇑a x = 0) l

source
def poly.remap {α : Type u_1} {β : Type u_2} (f : α → β) (g : poly α) :
poly β

Map the index set of variables, replacing x_i with x_(f i).

Equations
source
@[simp]
theorem poly.remap_eval {α : Type u_1} {β : Type u_2} (f : α → β) (g : poly α) (v : β → ℕ) :
⇑(poly.remap f g) v = ⇑g (v ∘ f)

source
def sum.join {α : Type u_1} {β : Type u_2} {γ : Sort u_3} (f : α → γ) (g : β → γ) (a : α ⊕ β) :
γ

combine two functions into a function on the disjoint union

Equations
source
def option.cons {α : Type u_1} {β : Sort u_2} (a : β) (v : α → β) (a_1 : option α) :
β

Functions from option can be combined similarly to vector.cons

Equations
  • a :: v = option.rec a v
source
@[simp]
theorem option.cons_head_tail {α : Type u_1} {β : Sort u_2} (v : option α → β) :
v none :: v ∘ some = v

source
def dioph {α : Type u} (S : 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.

Equations
source
theorem dioph.ext {α : Type u} {S S' : set (α → ℕ)} (d : dioph S) (H : ∀ (v : α → ℕ), S v ↔ S' v) :
dioph S'

source
theorem dioph.of_no_dummies {α : Type u} (S : set (α → ℕ)) (p : poly α) (h : ∀ (v : α → ℕ), S v ↔ ⇑p v = 0) :
dioph S

source
theorem dioph.inject_dummies_lem {α β γ : Type u} (f : β → γ) (g : γ → option β) (inv : ∀ (x : β), g (f x) = some x) (p : poly (α ⊕ β)) (v : α → ℕ) :
(∃ (t : β → ℕ), ⇑p (sum.join v t) = 0) ↔ ∃ (t : γ → ℕ), ⇑(poly.remap (sum.join sum.inl (sum.inr ∘ f)) p) (sum.join v t) = 0

source
theorem dioph.inject_dummies {α β γ : Type u} {S : set (α → ℕ)} (f : β → γ) (g : γ → option β) (inv : ∀ (x : β), g (f x) = some x) (p : poly (α ⊕ β)) (h : ∀ (v : α → ℕ), S v ↔ ∃ (t : β → ℕ), ⇑p (sum.join v t) = 0) :
∃ (q : poly (α ⊕ γ)), ∀ (v : α → ℕ), S v ↔ ∃ (t : γ → ℕ), ⇑q (sum.join v t) = 0

source
theorem dioph.reindex_dioph {α β : Type u} {S : set (α → ℕ)} (d : dioph S) (f : α → β) :
dioph (λ (v : β → ℕ), S (v ∘ f))

source
theorem dioph.dioph_list_all {α : Type u} (l : list (set (α → ℕ))) (d : list_all dioph l) :
dioph (λ (v : α → ℕ), list_all (λ (S : set (α → ℕ)), S v) l)

source
theorem dioph.and_dioph {α : Type u} {S S' : set (α → ℕ)} (d : dioph S) (d' : dioph S') :
dioph (λ (v : α → ℕ), S v ∧ S' v)

source
theorem dioph.or_dioph {α : Type u} {S S' : set (α → ℕ)} (d : dioph S) (d' : dioph S') :
dioph (λ (v : α → ℕ), S v ∨ S' v)

source
def dioph.dioph_pfun {α : Type u} (f : (α → ℕ) →. ℕ) :
Prop

A partial function is Diophantine if its graph is Diophantine.

Equations
source
def dioph.dioph_fn {α : Type u} (f : (α → ℕ) → ℕ) :
Prop

A function is Diophantine if its graph is Diophantine.

Equations
source
theorem dioph.reindex_dioph_fn {α β : Type u} {f : (α → ℕ) → ℕ} (d : dioph.dioph_fn f) (g : α → β) :
dioph.dioph_fn (λ (v : β → ℕ), f (v ∘ g))

source
theorem dioph.ex_dioph {α β : Type u} {S : set (α ⊕ β → ℕ)} (a : dioph S) :
dioph (λ (v : α → ℕ), ∃ (x : β → ℕ), S (sum.join v x))

source
theorem dioph.ex1_dioph {α : Type u} {S : set (option α → ℕ)} (a : dioph S) :
dioph (λ (v : α → ℕ), ∃ (x : ℕ), S (x :: v))

source
theorem dioph.dom_dioph {α : Type u} {f : (α → ℕ) →. ℕ} (d : dioph.dioph_pfun f) :
dioph f.dom

source
theorem dioph.dioph_fn_iff_pfun {α : Type u} (f : (α → ℕ) → ℕ) :
dioph.dioph_fn f = dioph.dioph_pfun ↑f

source
theorem dioph.abs_poly_dioph {α : Type u} (p : poly α) :
dioph.dioph_fn (λ (v : α → ℕ), (⇑p v).nat_abs)

source
theorem dioph.proj_dioph {α : Type u} (i : α) :
dioph.dioph_fn (λ (v : α → ℕ), v i)

source
theorem dioph.dioph_pfun_comp1 {α : Type u} {S : set (option α → ℕ)} (d : dioph S) {f : (α → ℕ) →. ℕ} (df : dioph.dioph_pfun f) :
dioph (λ (v : α → ℕ), ∃ (h : f.dom v), S (f.fn v h :: v))

source
theorem dioph.dioph_fn_comp1 {α : Type u} {S : set (option α → ℕ)} (d : dioph S) {f : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) :
dioph (λ (v : α → ℕ), S (f v :: v))

source
theorem dioph.dioph_fn_vec_comp1 {n : ℕ} {S : set (vector3 ℕ n.succ)} (d : dioph S) {f : vector3 ℕ n → ℕ} (df : dioph.dioph_fn f) :
dioph (λ (v : vector3 ℕ n), S (f v :: v))

source
theorem dioph.vec_ex1_dioph (n : ℕ) {S : set (vector3 ℕ n.succ)} (d : dioph S) :
dioph (λ (v : vector3 ℕ n), ∃ (x : ℕ), S (x :: v))

source
theorem dioph.dioph_fn_vec {n : ℕ} (f : vector3 ℕ n → ℕ) :
dioph.dioph_fn f ↔ dioph (λ (v : vector3 ℕ n.succ), f (v ∘ fin2.fs) = v fin2.fz)

source
theorem dioph.dioph_pfun_vec {n : ℕ} (f : vector3 ℕ n →. ℕ) :
dioph.dioph_pfun f ↔ dioph (λ (v : vector3 ℕ n.succ), f.graph (v ∘ fin2.fs, v fin2.fz))

source
theorem dioph.dioph_fn_compn {α : Type} {n : ℕ} {S : set (α ⊕ fin2 n → ℕ)} (d : dioph S) {f : vector3 ((α → ℕ) → ℕ) n} (df : vector_allp dioph.dioph_fn f) :
dioph (λ (v : α → ℕ), S (sum.join v (λ (i : fin2 n), f i v)))

source
theorem dioph.dioph_comp {α : Type} {n : ℕ} {S : set (vector3 ℕ n)} (d : dioph S) (f : vector3 ((α → ℕ) → ℕ) n) (df : vector_allp dioph.dioph_fn f) :
dioph (λ (v : α → ℕ), S (λ (i : fin2 n), f i v))

source
theorem dioph.dioph_fn_comp {α : Type} {n : ℕ} {f : vector3 ℕ n → ℕ} (df : dioph.dioph_fn f) (g : vector3 ((α → ℕ) → ℕ) n) (dg : vector_allp dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), f (λ (i : fin2 n), g i v))

source
theorem dioph.proj_dioph_of_nat {n : ℕ} (m : ℕ) [fin2.is_lt m n] :
dioph.dioph_fn (λ (v : vector3 ℕ n), v (fin2.of_nat' m))

source
theorem dioph.const_dioph {α : Type} (n : ℕ) :
dioph.dioph_fn (function.const (α → ℕ) n)

source
theorem dioph.dioph_comp2 {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {S : ℕ → ℕ → Prop} (d : dioph (λ (v : vector3 ℕ 2), S (v (fin2.of_nat' 0)) (v (fin2.of_nat' 1)))) :
dioph (λ (v : α → ℕ), S (f v) (g v))

source
theorem dioph.dioph_fn_comp2 {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {h : ℕ → ℕ → ℕ} (d : dioph.dioph_fn (λ (v : vector3 ℕ 2), h (v (fin2.of_nat' 0)) (v (fin2.of_nat' 1)))) :
dioph.dioph_fn (λ (v : α → ℕ), h (f v) (g v))

source
theorem dioph.eq_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph (λ (v : α → ℕ), f v = g v)

source
theorem dioph.add_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), f v + g v)

source
theorem dioph.mul_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), (f v) * g v)

source
theorem dioph.le_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph (λ (v : α → ℕ), f v ≤ g v)

source
theorem dioph.lt_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph (λ (v : α → ℕ), f v < g v)

source
theorem dioph.ne_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph (λ (v : α → ℕ), f v ≠ g v)

source
theorem dioph.sub_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), f v - g v)

source
theorem dioph.dvd_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph (λ (v : α → ℕ), f v ∣ g v)

source
theorem dioph.mod_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), f v % g v)

source
theorem dioph.modeq_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {h : (α → ℕ) → ℕ} (dh : dioph.dioph_fn h) :
dioph (λ (v : α → ℕ), f v ≡ g v [MOD h v])

source
theorem dioph.div_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), f v / g v)

source
theorem dioph.pell_dioph  :
dioph (λ (v : vector3 ℕ 4), ∃ (h : 1 < v (fin2.of_nat' 0)), pell.xn h (v (fin2.of_nat' 1)) = v (fin2.of_nat' 2) ∧ pell.yn h (v (fin2.of_nat' 1)) = v (fin2.of_nat' 3))

source
theorem dioph.xn_dioph  :
dioph.dioph_pfun (λ (v : vector3 ℕ 2), {dom := 1 < v (fin2.of_nat' 0), get := λ (h : 1 < v (fin2.of_nat' 0)), pell.xn h (v (fin2.of_nat' 1))})

source
theorem dioph.pow_dioph {α : Type} {f g : (α → ℕ) → ℕ} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) :
dioph.dioph_fn (λ (v : α → ℕ), f v ^ g v)