mathlib docs: number

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

C vector3.nil → (Π {n : ℕ} (a : α) (w : vector3 α n), C w → C (a :: w)) → C v

Equations

v.rec_on H0 Hs = n.rec_on (λ (v : vector3 α 0), vector3.nil_elim H0 v) (λ (n : ℕ) (IH : Π (_a : vector3 α n), C _a) (v : vector3 α n.succ), vector3.cons_elim (λ (a : α) (t : vector3 α n), Hs a t (IH t)) v) v

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 : ℕ} :

vector3 α n → vector3 α (n + m)

Append two vectors

Equations

v.append w = m.rec_on (λ (_x : vector3 α 0), w) (λ (m : ℕ) (IH : vector3 α m → vector3 α (n + m)) (v : vector3 α m.succ), vector3.cons_elim (λ (a : α) (t : vector3 α m), fin2.cases' a (IH t)) v) v

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 : ℕ} :

vector3 α n → fin2 n.succ → vector3 α n.succ

Insert a into v at index i.

Equations

vector3.insert a v i = λ (j : fin2 n.succ), (a :: v) (i.insert_perm j)

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

(vector3 α k → Prop) → Prop

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

Equations

vector_ex k.succ f = ∃ (x : α), vector_ex k (λ (v : vector3 α k), f (x :: v))
vector_ex 0 f = f vector3.nil

source

def vector_all {α : Type u_1} (k : ℕ) :

(vector3 α k → Prop) → Prop

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

Equations

vector_all k.succ f = ∀ (x : α), vector_all k (λ (v : vector3 α k), f (x :: v))
vector_all 0 f = f vector3.nil

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 : ℕ} :

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

vector_allp p v = v.rec_on true (λ (n : ℕ) (a : α) (v : vector3 α n) (IH : Prop), v.rec_on (p a) (λ (n : ℕ) (b : α) (v' : vector3 α n) (_x : (λ (n : ℕ) (v : vector3 α n), Prop) n v'), p a ∧ IH))

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

vector_allp p v → vector_allp q v

source

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

list_all p (x :: hd :: tl) = (p x ∧ list_all p (hd :: tl))
list_all p [x] = p x
list_all p list.nil = true

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 α} :

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

decidable_list_all p l = decidable_of_decidable_of_iff (list.decidable_ball (λ (x : α), p x) l) _

source

inductive is_poly {α : Sort u_1} :

((α → ℕ) → ℤ) → Prop

proj : ∀ {α : Sort u_1} (i : α), is_poly (λ (x : α → ℕ), ↑(x i))
const : ∀ {α : Sort u_1} (n : ℤ), is_poly (λ (x : α → ℕ), n)
sub : ∀ {α : Sort u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), f x - g x)
mul : ∀ {α : Sort u_1} {f g : (α → ℕ) → ℤ}, is_poly f → is_poly g → is_poly (λ (x : α → ℕ), f x * g x)

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

poly α = {f // is_poly f}

source

@[instance]

def poly.has_coe_to_fun {α : Type u} :

has_coe_to_fun (poly α)

Equations

poly.has_coe_to_fun = {F := λ (f : poly α), (α → ℕ) → ℤ, coe := λ (f : poly α), f.val}

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 α} :

(∀ (x : α → ℕ), ⇑f x = ⇑g x) → f = g

Extensionality for poly α

source

def poly.subst {α : Type u} (f : poly α) (g : (α → ℕ) → ℤ) :

(∀ (x : α → ℕ), ⇑f x = g x) → poly α

Construct a poly given an extensionally equivalent poly.

Equations

f.subst g e = ⟨g, _⟩

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

α → poly α

The ith projection function, x_i.

Equations

poly.proj i = ⟨λ (x : α → ℕ), ↑(x i), _⟩

source

@[simp]

theorem poly.proj_eval {α : Type u} (i : α) (x : α → ℕ) :

⇑(poly.proj i) x = ↑(x i)

source

def poly.const {α : Type u} :

ℤ → poly α

The constant function with value n : ℤ.

Equations

poly.const n = ⟨λ (x : α → ℕ), n, _⟩

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

poly.zero = poly.const 0

source

@[instance]

def poly.has_zero {α : Type u} :

has_zero (poly α)

Equations

poly.has_zero = {zero := poly.zero α}

source

@[simp]

theorem poly.zero_eval {α : Type u} (x : α → ℕ) :

⇑0 x = 0

source

def poly.one {α : Type u} :

poly α

The zero polynomial

Equations

poly.one = poly.const 1

source

@[instance]

def poly.has_one {α : Type u} :

has_one (poly α)

Equations

poly.has_one = {one := poly.one α}

source

@[simp]

theorem poly.one_eval {α : Type u} (x : α → ℕ) :

⇑1 x = 1

source

def poly.sub {α : Type u} :

poly α → poly α → poly α

Subtraction of polynomials

Equations

poly.sub ⟨f, pf⟩ ⟨g, pg⟩ = ⟨λ (x : α → ℕ), f x - g x, _⟩

source

@[instance]

def poly.has_sub {α : Type u} :

has_sub (poly α)

Equations

poly.has_sub = {sub := poly.sub α}

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

poly α → poly α

Negation of a polynomial

Equations

f.neg = 0 - f

source

@[instance]

def poly.has_neg {α : Type u} :

has_neg (poly α)

Equations

poly.has_neg = {neg := poly.neg α}

source

@[simp]

theorem poly.neg_eval {α : Type u} (f : poly α) (x : α → ℕ) :

(⇑-f) x = -⇑f x

source

def poly.add {α : Type u} :

poly α → poly α → poly α

Addition of polynomials

Equations

poly.add ⟨f, pf⟩ ⟨g, pg⟩ = (⟨f, pf⟩ - -⟨g, pg⟩).subst (λ (x : α → ℕ), f x + g x) _

source

@[instance]

def poly.has_add {α : Type u} :

has_add (poly α)

Equations

poly.has_add = {add := poly.add α}

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

poly α → poly α → poly α

Multiplication of polynomials

Equations

poly.mul ⟨f, pf⟩ ⟨g, pg⟩ = ⟨λ (x : α → ℕ), f x * g x, _⟩

source

@[instance]

def poly.has_mul {α : Type u} :

has_mul (poly α)

Equations

poly.has_mul = {mul := poly.mul α}

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

poly.comm_ring = {add := has_add.add poly.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, neg := has_neg.neg poly.has_neg, add_left_neg := _, add_comm := _, mul := has_mul.mul poly.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _, mul_comm := _}

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

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

poly.sumsq (p :: ps) = p * p + poly.sumsq ps
poly.sumsq list.nil = 0

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

(α → β) → poly α → poly β

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

Equations

poly.remap f g = ⟨λ (v : β → ℕ), ⇑g (v ∘ f), _⟩

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

(α → γ) → (β → γ) → α ⊕ β → γ

combine two functions into a function on the disjoint union

Equations

sum.join f g = sum.rec f g

source

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

source

@[simp]

theorem option.cons_head_tail {α : Type u_1} {β : Sort u_2} (v : option α → β) :

v option.none :: v ∘ option.some = v

source

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

dioph S = ∃ {β : Type u} (p : poly (α ⊕ β)), ∀ (v : α → ℕ), S v ↔ ∃ (t : β → ℕ), ⇑p (sum.join v t) = 0

source

theorem dioph.ext {α : Type u} {S S' : set (α → ℕ)} :

dioph S → (∀ (v : α → ℕ), S v ↔ S' v) → dioph S'

source

theorem dioph.of_no_dummies {α : Type u} (S : set (α → ℕ)) (p : poly α) :

(∀ (v : α → ℕ), S v ↔ ⇑p v = 0) → dioph S

source

theorem dioph.inject_dummies_lem {α β γ : Type u} (f : β → γ) (g : γ → option β) (inv : ∀ (x : β), g (f x) = option.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) = option.some x) (p : poly (α ⊕ β)) :