mathlib documentation

number_theory.dioph

theorem int.eq_nat_abs_iff_mul (x : ) (n : ) :
x.nat_abs = n (x - n) * (x + n) = 0

def vector3  :
Type uType u

Alternate definition of vector based on fin2.

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

The empty vector

def vector3.cons {α : Type u_1} {n : } :
α → vector3 α nvector3 α n.succ

The vector cons operation

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

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

def vector3.nth {α : Type u_1} {n : } :
fin2 nvector3 α n → α

Get the ith element of a vector

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

Construct a vector from a function on fin2.

Equations
def vector3.head {α : Type u_1} {n : } :
vector3 α n.succ → α

Get the head of a nonempty vector.

Equations
def vector3.tail {α : Type u_1} {n : } :
vector3 α n.succvector3 α n

Get the tail of a nonempty vector.

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

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

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

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

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

def vector3.rec_on {α : Type u_1} {C : Π {n : }, vector3 α nSort u} {n : } (v : vector3 α n) :
C vector3.nil(Π {n : } (a : α) (w : vector3 α n), C wC (a :: w))C v

Equations
@[simp]
theorem vector3.rec_on_nil {α : Type u_1} {C : Π {n : }, vector3 α nSort u_2} {H0 : C vector3.nil} {Hs : Π {n : } (a : α) (w : vector3 α n), C wC (a :: w)} :

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

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

Append two vectors

Equations
@[simp]
theorem vector3.append_nil {α : Type u_1} {n : } (w : vector3 α n) :

@[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

@[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

@[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

def vector3.insert {α : Type u_1} (a : α) {n : } :
vector3 α nfin2 n.succvector3 α n.succ

Insert a into v at index i.

Equations
@[simp]
theorem vector3.insert_fz {α : Type u_1} (a : α) {n : } (v : vector3 α n) :

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

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))

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

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

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

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

Equations
theorem exists_vector_zero {α : Type u_1} (f : vector3 α 0 → Prop) :

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

theorem vector_ex_iff_exists {α : Type u_1} {n : } (f : vector3 α n → Prop) :

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

def vector_allp {α : Type u_1} (p : α → Prop) {n : } :
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
@[simp]
theorem vector_allp_nil {α : Type u_1} (p : α → Prop) :

@[simp]
theorem vector_allp_singleton {α : Type u_1} (p : α → Prop) (x : α) :

@[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

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

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

@[simp]
def list_all {α : Type u_1} :
(α → Prop)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
@[simp]
theorem list_all_cons {α : Type u_1} (p : α → Prop) (x : α) (l : list α) :
list_all p (x :: l) p x list_all p l

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

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

@[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

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

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

Equations
inductive is_poly {α : Sort u_1} :
((α → )) → 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.)

def poly  :
Type uType u

The type of multivariate integer polynomials

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

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

The underlying function of a poly is a polynomial

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

Extensionality for poly α

def poly.subst {α : Type u} (f : poly α) (g : (α → )) :
(∀ (x : α → ), f x = g x)poly α

Construct a poly given an extensionally equivalent poly.

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

def poly.proj {α : Type u} :
α → poly α

The ith projection function, x_i.

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

def poly.const {α : Type u} :
poly α

The constant function with value n : ℤ.

Equations
@[simp]
theorem poly.const_eval {α : Type u} (n : ) (x : α → ) :

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

The zero polynomial

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

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

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

The zero polynomial

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

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

def poly.sub {α : Type u} :
poly αpoly αpoly α

Subtraction of polynomials

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

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

def poly.neg {α : Type u} :
poly αpoly α

Negation of a polynomial

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

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

def poly.add {α : Type u} :
poly αpoly αpoly α

Addition of polynomials

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

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

def poly.mul {α : Type u} :
poly αpoly αpoly α

Multiplication of polynomials

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

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

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

Equations
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 fC gC (f - g)) (H4 : ∀ (f g : poly α), C fC gC (f * g)) (f : poly α) :
C f

def poly.sumsq {α : Type u} :
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
theorem poly.sumsq_nonneg {α : Type u} (x : α → ) (l : list (poly α)) :

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

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

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

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

def sum.join {α : Type u_1} {β : Type u_2} {γ : Sort u_3} :
(α → γ)(β → γ)α β → γ

combine two functions into a function on the disjoint union

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

Functions from option can be combined similarly to vector.cons

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

def 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.

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

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

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

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

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

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

theorem dioph.and_dioph {α : Type u} {S S' : set (α → )} :
dioph Sdioph S'dioph (λ (v : α → ), S v S' v)

theorem dioph.or_dioph {α : Type u} {S S' : set (α → )} :
dioph Sdioph S'dioph (λ (v : α → ), S v S' v)

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

A partial function is Diophantine if its graph is Diophantine.

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

A function is Diophantine if its graph is Diophantine.

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

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

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

theorem dioph.dom_dioph {α : Type u} {f : (α → ) →. } :

theorem dioph.dioph_fn_iff_pfun {α : Type u} (f : (α → )) :

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

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

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

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

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

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

theorem dioph.dioph_fn_vec {n : } (f : vector3 n) :

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

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

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

theorem dioph.proj_dioph_of_nat {n : } (m : ) [fin2.is_lt m n] :

theorem dioph.const_dioph {α : Type} (n : ) :

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

theorem dioph.dioph_fn_comp2 {α : Type} {f g : (α → )} (df : dioph.dioph_fn f) (dg : dioph.dioph_fn g) {h : } :
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))

theorem dioph.eq_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph (λ (v : α → ), f v = g v)

theorem dioph.add_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph.dioph_fn (λ (v : α → ), f v + g v)

theorem dioph.mul_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph.dioph_fn (λ (v : α → ), (f v) * g v)

theorem dioph.le_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph (λ (v : α → ), f v g v)

theorem dioph.lt_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph (λ (v : α → ), f v < g v)

theorem dioph.ne_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph (λ (v : α → ), f v g v)

theorem dioph.sub_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph.dioph_fn (λ (v : α → ), f v - g v)

theorem dioph.dvd_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph (λ (v : α → ), f v g v)

theorem dioph.mod_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph.dioph_fn (λ (v : α → ), f v % g v)

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

theorem dioph.div_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph.dioph_fn (λ (v : α → ), f v / g v)

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))

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))})

theorem dioph.pow_dioph {α : Type} {f g : (α → )} :
dioph.dioph_fn fdioph.dioph_fn gdioph.dioph_fn (λ (v : α → ), f v ^ g v)