mathlib documentation

data.zsqrtd.basic

structure zsqrtd  :
→ Type

The ring of integers adjoined with a square root of d. These have the form a + b √d where a b : ℤ. The components are called re and im by analogy to the negative d case, but of course both parts are real here since d is nonnegative.

@[instance]

Equations
theorem zsqrtd.ext {d : } {z w : ℤ√d} :
z = w z.re = w.re z.im = w.im

def zsqrtd.of_int {d : } :
ℤ√d

Convert an integer to a ℤ√d

Equations
theorem zsqrtd.of_int_re {d : } (n : ) :

theorem zsqrtd.of_int_im {d : } (n : ) :

def zsqrtd.zero {d : } :

The zero of the ring

Equations
@[instance]

Equations
@[simp]
theorem zsqrtd.zero_re {d : } :
0.re = 0

@[simp]
theorem zsqrtd.zero_im {d : } :
0.im = 0

@[instance]

Equations
def zsqrtd.one {d : } :

The one of the ring

Equations
@[instance]
def zsqrtd.has_one {d : } :

Equations
@[simp]
theorem zsqrtd.one_re {d : } :
1.re = 1

@[simp]
theorem zsqrtd.one_im {d : } :
1.im = 0

def zsqrtd.sqrtd {d : } :

The representative of √d in the ring

Equations
@[simp]
theorem zsqrtd.sqrtd_re {d : } :

@[simp]
theorem zsqrtd.sqrtd_im {d : } :

def zsqrtd.add {d : } :
ℤ√d → ℤ√d → ℤ√d

Addition of elements of ℤ√d

Equations
@[instance]
def zsqrtd.has_add {d : } :

Equations
@[simp]
theorem zsqrtd.add_def {d : } (x y x' y' : ) :
{re := x, im := y} + {re := x', im := y'} = {re := x + x', im := y + y'}

@[simp]
theorem zsqrtd.add_re {d : } (z w : ℤ√d) :
(z + w).re = z.re + w.re

@[simp]
theorem zsqrtd.add_im {d : } (z w : ℤ√d) :
(z + w).im = z.im + w.im

@[simp]
theorem zsqrtd.bit0_re {d : } (z : ℤ√d) :
(bit0 z).re = bit0 z.re

@[simp]
theorem zsqrtd.bit0_im {d : } (z : ℤ√d) :
(bit0 z).im = bit0 z.im

@[simp]
theorem zsqrtd.bit1_re {d : } (z : ℤ√d) :
(bit1 z).re = bit1 z.re

@[simp]
theorem zsqrtd.bit1_im {d : } (z : ℤ√d) :
(bit1 z).im = bit0 z.im

def zsqrtd.neg {d : } :

Negation in ℤ√d

Equations
@[instance]
def zsqrtd.has_neg {d : } :

Equations
@[simp]
theorem zsqrtd.neg_re {d : } (z : ℤ√d) :
(-z).re = -z.re

@[simp]
theorem zsqrtd.neg_im {d : } (z : ℤ√d) :
(-z).im = -z.im

def zsqrtd.conj {d : } :

Conjugation in ℤ√d. The conjugate of a + b √d is a - b √d.

Equations
@[simp]
theorem zsqrtd.conj_re {d : } (z : ℤ√d) :
z.conj.re = z.re

@[simp]
theorem zsqrtd.conj_im {d : } (z : ℤ√d) :
z.conj.im = -z.im

def zsqrtd.mul {d : } :
ℤ√d → ℤ√d → ℤ√d

Multiplication in ℤ√d

Equations
@[instance]
def zsqrtd.has_mul {d : } :

Equations
@[simp]
theorem zsqrtd.mul_re {d : } (z w : ℤ√d) :
(z * w).re = (z.re) * w.re + (d * z.im) * w.im

@[simp]
theorem zsqrtd.mul_im {d : } (z w : ℤ√d) :
(z * w).im = (z.re) * w.im + (z.im) * w.re

@[instance]
def zsqrtd.monoid {d : } :

Equations
@[instance]

Equations
@[instance]
def zsqrtd.ring {d : } :

Equations
@[instance]
def zsqrtd.distrib {d : } :

Equations
@[instance]

@[simp]
theorem zsqrtd.coe_nat_re {d : } (n : ) :

@[simp]
theorem zsqrtd.coe_nat_im {d : } (n : ) :
n.im = 0

theorem zsqrtd.coe_nat_val {d : } (n : ) :
n = {re := n, im := 0}

@[simp]
theorem zsqrtd.coe_int_re {d : } (n : ) :
n.re = n

@[simp]
theorem zsqrtd.coe_int_im {d : } (n : ) :
n.im = 0

theorem zsqrtd.coe_int_val {d : } (n : ) :
n = {re := n, im := 0}

@[instance]

@[simp]
theorem zsqrtd.of_int_eq_coe {d : } (n : ) :

@[simp]
theorem zsqrtd.smul_val {d : } (n x y : ) :
(n) * {re := x, im := y} = {re := n * x, im := n * y}

@[simp]
theorem zsqrtd.muld_val {d : } (x y : ) :
zsqrtd.sqrtd * {re := x, im := y} = {re := d * y, im := x}

@[simp]
theorem zsqrtd.smuld_val {d : } (n x y : ) :
(zsqrtd.sqrtd * n) * {re := x, im := y} = {re := (d * n) * y, im := n * x}

theorem zsqrtd.decompose {d x y : } :
{re := x, im := y} = x + zsqrtd.sqrtd * y

theorem zsqrtd.mul_conj {d x y : } :
{re := x, im := y} * {re := x, im := y}.conj = (x) * x - ((d) * y) * y

theorem zsqrtd.conj_mul {d : } {a b : ℤ√d} :
(a * b).conj = (a.conj) * b.conj

theorem zsqrtd.coe_int_add {d : } (m n : ) :
(m + n) = m + n

theorem zsqrtd.coe_int_sub {d : } (m n : ) :
(m - n) = m - n

theorem zsqrtd.coe_int_mul {d : } (m n : ) :
m * n = (m) * n

theorem zsqrtd.coe_int_inj {d m n : } :
m = nm = n

def zsqrtd.sq_le  :
→ Prop

Read sq_le a c b d as a √c ≤ b √d

Equations
theorem zsqrtd.sq_le_of_le {c d x y z w : } :
z xy wzsqrtd.sq_le x c y dzsqrtd.sq_le z c w d

theorem zsqrtd.sq_le_add_mixed {c d x y z w : } :
zsqrtd.sq_le x c y dzsqrtd.sq_le z c w dc * x * z d * y * w

theorem zsqrtd.sq_le_add {c d x y z w : } :
zsqrtd.sq_le x c y dzsqrtd.sq_le z c w dzsqrtd.sq_le (x + z) c (y + w) d

theorem zsqrtd.sq_le_cancel {c d x y z w : } :
zsqrtd.sq_le y d x czsqrtd.sq_le (x + z) c (y + w) dzsqrtd.sq_le z c w d

theorem zsqrtd.sq_le_smul {c d x y : } (n : ) :
zsqrtd.sq_le x c y dzsqrtd.sq_le (n * x) c (n * y) d

theorem zsqrtd.sq_le_mul {d x y z w : } :
(zsqrtd.sq_le x 1 y dzsqrtd.sq_le z 1 w dzsqrtd.sq_le (x * w + y * z) d (x * z + (d * y) * w) 1) (zsqrtd.sq_le x 1 y dzsqrtd.sq_le w d z 1zsqrtd.sq_le (x * z + (d * y) * w) 1 (x * w + y * z) d) (zsqrtd.sq_le y d x 1zsqrtd.sq_le z 1 w dzsqrtd.sq_le (x * z + (d * y) * w) 1 (x * w + y * z) d) (zsqrtd.sq_le y d x 1zsqrtd.sq_le w d z 1zsqrtd.sq_le (x * w + y * z) d (x * z + (d * y) * w) 1)

def zsqrtd.nonnegg  :
→ Prop

"Generalized" nonneg. nonnegg c d x y means a √c + b √d ≥ 0; we are interested in the case c = 1 but this is more symmetric

Equations
theorem zsqrtd.nonnegg_comm {c d : } {x y : } :

theorem zsqrtd.nonnegg_neg_pos {c d a b : } :

theorem zsqrtd.nonnegg_pos_neg {c d a b : } :

theorem zsqrtd.nonnegg_cases_right {c d a : } {b : } :
(∀ (x : ), b = -xzsqrtd.sq_le x c a d)zsqrtd.nonnegg c d a b

theorem zsqrtd.nonnegg_cases_left {c d b : } {a : } :
(∀ (x : ), a = -xzsqrtd.sq_le x d b c)zsqrtd.nonnegg c d a b

def zsqrtd.norm {d : } :
ℤ√d →

Equations
@[simp]
theorem zsqrtd.norm_zero {d : } :
0.norm = 0

@[simp]
theorem zsqrtd.norm_one {d : } :
1.norm = 1

@[simp]
theorem zsqrtd.norm_int_cast {d : } (n : ) :
n.norm = n * n

@[simp]
theorem zsqrtd.norm_nat_cast {d : } (n : ) :
n.norm = (n) * n

@[simp]
theorem zsqrtd.norm_mul {d : } (n m : ℤ√d) :
(n * m).norm = (n.norm) * m.norm

theorem zsqrtd.norm_eq_mul_conj {d : } (n : ℤ√d) :
(n.norm) = n * n.conj

theorem zsqrtd.norm_nonneg {d : } (hd : d 0) (n : ℤ√d) :
0 n.norm

theorem zsqrtd.norm_eq_one_iff {d : } {x : ℤ√d} :

def zsqrtd.nonneg {d : } :
ℤ√d → Prop

Nonnegativity of an element of ℤ√d.

Equations
def zsqrtd.le {d : } :
ℤ√d → ℤ√d → Prop

Equations
@[instance]
def zsqrtd.has_le {d : } :

Equations
def zsqrtd.lt {d : } :
ℤ√d → ℤ√d → Prop

Equations
@[instance]
def zsqrtd.has_lt {d : } :

Equations
@[instance]
def zsqrtd.decidable_nonnegg (c d : ) (a b : ) :

Equations
@[instance]

Equations
@[instance]
def zsqrtd.decidable_le {d : } (a b : ℤ√d) :

Equations
theorem zsqrtd.nonneg_cases {d : } {a : ℤ√d} :
a.nonneg(∃ (x y : ), a = {re := x, im := y} a = {re := x, im := -y} a = {re := -x, im := y})

theorem zsqrtd.nonneg_add_lem {d x y z w : } :
{re := x, im := -y}.nonneg{re := -z, im := w}.nonneg({re := x, im := -y} + {re := -z, im := w}).nonneg

theorem zsqrtd.nonneg_add {d : } {a b : ℤ√d} :
a.nonnegb.nonneg(a + b).nonneg

theorem zsqrtd.le_refl {d : } (a : ℤ√d) :
a a

theorem zsqrtd.le_trans {d : } {a b c : ℤ√d} :
a bb ca c

theorem zsqrtd.nonneg_iff_zero_le {d : } {a : ℤ√d} :
a.nonneg 0 a

theorem zsqrtd.le_of_le_le {d : } {x y z w : } :
x zy w{re := x, im := y} {re := z, im := w}

theorem zsqrtd.le_arch {d : } (a : ℤ√d) :
∃ (n : ), a n

theorem zsqrtd.nonneg_total {d : } (a : ℤ√d) :

theorem zsqrtd.le_total {d : } (a b : ℤ√d) :
a b b a

@[instance]

Equations
theorem zsqrtd.add_le_add_left {d : } (a b : ℤ√d) (ab : a b) (c : ℤ√d) :
c + a c + b

theorem zsqrtd.le_of_add_le_add_left {d : } (a b c : ℤ√d) :
c + a c + ba b

theorem zsqrtd.add_lt_add_left {d : } (a b : ℤ√d) (h : a < b) (c : ℤ√d) :
c + a < c + b

theorem zsqrtd.nonneg_smul {d : } {a : ℤ√d} {n : } :
a.nonneg((n) * a).nonneg

theorem zsqrtd.nonneg_muld {d : } {a : ℤ√d} :

theorem zsqrtd.nonneg_mul_lem {d x y : } {a : ℤ√d} :
a.nonneg({re := x, im := y} * a).nonneg

theorem zsqrtd.nonneg_mul {d : } {a b : ℤ√d} :
a.nonnegb.nonneg(a * b).nonneg

theorem zsqrtd.mul_nonneg {d : } (a b : ℤ√d) :
0 a0 b0 a * b

theorem zsqrtd.not_sq_le_succ (c d y : ) :
0 < c¬zsqrtd.sq_le (y + 1) c 0 d

@[class]
structure zsqrtd.nonsquare  :
→ Prop

A nonsquare is a natural number that is not equal to the square of an integer. This is implemented as a typeclass because it's a necessary condition for much of the Pell equation theory.

Instances
theorem zsqrtd.d_pos {d : } [dnsq : zsqrtd.nonsquare d] :
0 < d

theorem zsqrtd.divides_sq_eq_zero {d : } [dnsq : zsqrtd.nonsquare d] {x y : } :
x * x = (d * y) * yx = 0 y = 0

theorem zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : zsqrtd.nonsquare d] {x y : } :
x * x = ((d) * y) * yx = 0 y = 0

theorem zsqrtd.not_divides_square {d : } [dnsq : zsqrtd.nonsquare d] (x y : ) :
(x + 1) * (x + 1) (d * (y + 1)) * (y + 1)

theorem zsqrtd.nonneg_antisymm {d : } [dnsq : zsqrtd.nonsquare d] {a : ℤ√d} :
a.nonneg(-a).nonnega = 0

theorem zsqrtd.le_antisymm {d : } [dnsq : zsqrtd.nonsquare d] {a b : ℤ√d} :
a bb aa = b

theorem zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : zsqrtd.nonsquare d] {a b : ℤ√d} :
a * b = 0a = 0 b = 0

theorem zsqrtd.mul_pos {d : } [dnsq : zsqrtd.nonsquare d] (a b : ℤ√d) :
0 < a0 < b0 < a * b