# Documentation

Mathlib.NumberTheory.Zsqrtd.Basic

# ℤ[√d] #

The ring of integers adjoined with a square root of d : ℤ.

After defining the norm, we show that it is a linearly ordered commutative ring, as well as an integral domain.

We provide the universal property, that ring homomorphisms ℤ√d →+* R correspond to choices of square roots of d in R.

structure Zsqrtd (d : ) :

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.

Instances For
instance instDecidableEqZsqrtd :
{d : } →
Instances For
theorem Zsqrtd.ext {d : } {z : ℤ√d} {w : ℤ√d} :
z = w z.re = w.re z.im = w.im
def Zsqrtd.ofInt {d : } (n : ) :

Convert an integer to a ℤ√d

Instances For
theorem Zsqrtd.ofInt_re {d : } (n : ) :
().re = n
theorem Zsqrtd.ofInt_im {d : } (n : ) :
().im = 0

The zero of the ring

@[simp]
theorem Zsqrtd.zero_re {d : } :
0.re = 0
@[simp]
theorem Zsqrtd.zero_im {d : } :
0.im = 0
instance Zsqrtd.instOneZsqrtd {d : } :

The one of the ring

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

Instances For
@[simp]
theorem Zsqrtd.sqrtd_re {d : } :
Zsqrtd.sqrtd.re = 0
@[simp]
theorem Zsqrtd.sqrtd_im {d : } :
Zsqrtd.sqrtd.im = 1
instance Zsqrtd.instAddZsqrtd {d : } :

Addition of elements of ℤ√d

@[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 : ℤ√d) (w : ℤ√d) :
(z + w).re = z.re + w.re
@[simp]
theorem Zsqrtd.add_im {d : } (z : ℤ√d) (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
instance Zsqrtd.instNegZsqrtd {d : } :

Negation in ℤ√d

@[simp]
theorem Zsqrtd.neg_re {d : } (z : ℤ√d) :
(-z).re = -z.re
@[simp]
theorem Zsqrtd.neg_im {d : } (z : ℤ√d) :
(-z).im = -z.im
instance Zsqrtd.instMulZsqrtd {d : } :

Multiplication in ℤ√d

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

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

@[simp]
theorem Zsqrtd.star_mk {d : } (x : ) (y : ) :
star { re := x, im := y } = { re := x, im := -y }
@[simp]
theorem Zsqrtd.star_re {d : } (z : ℤ√d) :
(star z).re = z.re
@[simp]
theorem Zsqrtd.star_im {d : } (z : ℤ√d) :
(star z).im = -z.im
@[simp]
theorem Zsqrtd.coe_nat_re {d : } (n : ) :
(n).re = n
@[simp]
theorem Zsqrtd.ofNat_re {d : } (n : ) [] :
().re = n
@[simp]
theorem Zsqrtd.coe_nat_im {d : } (n : ) :
(n).im = 0
@[simp]
theorem Zsqrtd.ofNat_im {d : } (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 }
@[simp]
theorem Zsqrtd.ofInt_eq_coe {d : } (n : ) :
= n
@[simp]
theorem Zsqrtd.smul_val {d : } (n : ) (x : ) (y : ) :
n * { re := x, im := y } = { re := n * x, im := n * y }
theorem Zsqrtd.smul_re {d : } (a : ) (b : ℤ√d) :
(a * b).re = a * b.re
theorem Zsqrtd.smul_im {d : } (a : ) (b : ℤ√d) :
(a * b).im = a * b.im
@[simp]
theorem Zsqrtd.muld_val {d : } (x : ) (y : ) :
Zsqrtd.sqrtd * { re := x, im := y } = { re := d * y, im := x }
@[simp]
theorem Zsqrtd.dmuld {d : } :
Zsqrtd.sqrtd * Zsqrtd.sqrtd = d
@[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_star {d : } {x : } {y : } :
{ re := x, im := y } * star { re := x, im := y } = x * x - d * y * y
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 : } (h : m = n) :
m = n
theorem Zsqrtd.coe_int_dvd_iff {d : } (z : ) (a : ℤ√d) :
z a z a.re z a.im
@[simp]
theorem Zsqrtd.coe_int_dvd_coe_int {d : } (a : ) (b : ) :
a b a b
theorem Zsqrtd.eq_of_smul_eq_smul_left {d : } {a : } {b : ℤ√d} {c : ℤ√d} (ha : a 0) (h : a * b = a * c) :
b = c
theorem Zsqrtd.gcd_eq_zero_iff {d : } (a : ℤ√d) :
Int.gcd a.re a.im = 0 a = 0
theorem Zsqrtd.gcd_pos_iff {d : } (a : ℤ√d) :
0 < Int.gcd a.re a.im a 0
theorem Zsqrtd.coprime_of_dvd_coprime {d : } {a : ℤ√d} {b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b a) :
IsCoprime b.re b.im
theorem Zsqrtd.exists_coprime_of_gcd_pos {d : } {a : ℤ√d} (hgcd : 0 < Int.gcd a.re a.im) :
b, a = ↑(Int.gcd a.re a.im) * b IsCoprime b.re b.im
def Zsqrtd.SqLe (a : ) (c : ) (b : ) (d : ) :

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

Instances For
theorem Zsqrtd.sqLe_of_le {c : } {d : } {x : } {y : } {z : } {w : } (xz : z x) (yw : y w) (xy : Zsqrtd.SqLe x c y d) :
Zsqrtd.SqLe z c w d
theorem Zsqrtd.sqLe_add_mixed {c : } {d : } {x : } {y : } {z : } {w : } (xy : Zsqrtd.SqLe x c y d) (zw : Zsqrtd.SqLe z c w d) :
c * (x * z) d * (y * w)
theorem Zsqrtd.sqLe_add {c : } {d : } {x : } {y : } {z : } {w : } (xy : Zsqrtd.SqLe x c y d) (zw : Zsqrtd.SqLe z c w d) :
Zsqrtd.SqLe (x + z) c (y + w) d
theorem Zsqrtd.sqLe_cancel {c : } {d : } {x : } {y : } {z : } {w : } (zw : Zsqrtd.SqLe y d x c) (h : Zsqrtd.SqLe (x + z) c (y + w) d) :
Zsqrtd.SqLe z c w d
theorem Zsqrtd.sqLe_smul {c : } {d : } {x : } {y : } (n : ) (xy : Zsqrtd.SqLe x c y d) :
Zsqrtd.SqLe (n * x) c (n * y) d
theorem Zsqrtd.sqLe_mul {d : } {x : } {y : } {z : } {w : } :
(Zsqrtd.SqLe x 1 y dZsqrtd.SqLe z 1 w dZsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1) (Zsqrtd.SqLe x 1 y dZsqrtd.SqLe w d z 1Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (Zsqrtd.SqLe y d x 1Zsqrtd.SqLe z 1 w dZsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (Zsqrtd.SqLe y d x 1Zsqrtd.SqLe w d z 1Zsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1)
def Zsqrtd.Nonnegg (c : ) (d : ) :
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

Instances For
theorem Zsqrtd.nonnegg_comm {c : } {d : } {x : } {y : } :
theorem Zsqrtd.nonnegg_neg_pos {c : } {d : } {a : } {b : } :
Zsqrtd.Nonnegg c d (-a) b Zsqrtd.SqLe a d b c
theorem Zsqrtd.nonnegg_pos_neg {c : } {d : } {a : } {b : } :
Zsqrtd.Nonnegg c d (a) (-b) Zsqrtd.SqLe b c a d
theorem Zsqrtd.nonnegg_cases_right {c : } {d : } {a : } {b : } :
(∀ (x : ), b = -xZsqrtd.SqLe x c a d) → Zsqrtd.Nonnegg c d (a) b
theorem Zsqrtd.nonnegg_cases_left {c : } {d : } {b : } {a : } (h : ∀ (x : ), a = -xZsqrtd.SqLe x d b c) :
Zsqrtd.Nonnegg c d a b
def Zsqrtd.norm {d : } (n : ℤ√d) :

The norm of an element of ℤ[√d].

Instances For
theorem Zsqrtd.norm_def {d : } (n : ℤ√d) :
= n.re * n.re - d * n.im * n.im
@[simp]
theorem Zsqrtd.norm_zero {d : } :
= 0
@[simp]
theorem Zsqrtd.norm_one {d : } :
= 1
@[simp]
theorem Zsqrtd.norm_int_cast {d : } (n : ) :
= n * n
@[simp]
theorem Zsqrtd.norm_nat_cast {d : } (n : ) :
= n * n
@[simp]
theorem Zsqrtd.norm_mul {d : } (n : ℤ√d) (m : ℤ√d) :
Zsqrtd.norm (n * m) =

norm as a MonoidHom.

Instances For
theorem Zsqrtd.norm_eq_mul_conj {d : } (n : ℤ√d) :
↑() = n * star n
@[simp]
theorem Zsqrtd.norm_neg {d : } (x : ℤ√d) :
@[simp]
theorem Zsqrtd.norm_conj {d : } (x : ℤ√d) :
theorem Zsqrtd.norm_nonneg {d : } (hd : d 0) (n : ℤ√d) :
0
theorem Zsqrtd.norm_eq_one_iff {d : } {x : ℤ√d} :
= 1
theorem Zsqrtd.norm_eq_one_iff' {d : } (hd : d 0) (z : ℤ√d) :
= 1
theorem Zsqrtd.norm_eq_zero_iff {d : } (hd : d < 0) (z : ℤ√d) :
= 0 z = 0
theorem Zsqrtd.norm_eq_of_associated {d : } (hd : d 0) {x : ℤ√d} {y : ℤ√d} (h : ) :
def Zsqrtd.Nonneg {d : } :
ℤ√dProp

Nonnegativity of an element of ℤ√d.

Instances For
instance Zsqrtd.decidableNonnegg (c : ) (d : ) (a : ) (b : ) :
instance Zsqrtd.decidableNonneg {d : } (a : ℤ√d) :
instance Zsqrtd.decidableLE {d : } :
DecidableRel fun x x_1 => x x_1
theorem Zsqrtd.nonneg_cases {d : } {a : ℤ√d} :
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 : } (xy : Zsqrtd.Nonneg { re := x, im := -y }) (zw : Zsqrtd.Nonneg { re := -z, im := w }) :
Zsqrtd.Nonneg ({ re := x, im := -y } + { re := -z, im := w })
theorem Zsqrtd.Nonneg.add {d : } {a : ℤ√d} {b : ℤ√d} (ha : ) (hb : ) :
theorem Zsqrtd.nonneg_iff_zero_le {d : } {a : ℤ√d} :
0 a
theorem Zsqrtd.le_of_le_le {d : } {x : } {y : } {z : } {w : } (xz : x z) (yw : y w) :
{ re := x, im := y } { re := z, im := w }
theorem Zsqrtd.nonneg_total {d : } (a : ℤ√d) :
theorem Zsqrtd.le_total {d : } (a : ℤ√d) (b : ℤ√d) :
a b b a
theorem Zsqrtd.le_arch {d : } (a : ℤ√d) :
n, a n
theorem Zsqrtd.add_le_add_left {d : } (a : ℤ√d) (b : ℤ√d) (ab : a b) (c : ℤ√d) :
c + a c + b
theorem Zsqrtd.le_of_add_le_add_left {d : } (a : ℤ√d) (b : ℤ√d) (c : ℤ√d) (h : c + a c + b) :
a b
theorem Zsqrtd.add_lt_add_left {d : } (a : ℤ√d) (b : ℤ√d) (h : a < b) (c : ℤ√d) :
c + a < c + b
theorem Zsqrtd.nonneg_smul {d : } {a : ℤ√d} {n : } (ha : ) :
Zsqrtd.Nonneg (n * a)
theorem Zsqrtd.nonneg_muld {d : } {a : ℤ√d} (ha : ) :
Zsqrtd.Nonneg (Zsqrtd.sqrtd * a)
theorem Zsqrtd.nonneg_mul_lem {d : } {x : } {y : } {a : ℤ√d} (ha : ) :
Zsqrtd.Nonneg ({ re := x, im := y } * a)
theorem Zsqrtd.nonneg_mul {d : } {a : ℤ√d} {b : ℤ√d} (ha : ) (hb : ) :
theorem Zsqrtd.mul_nonneg {d : } (a : ℤ√d) (b : ℤ√d) :
0 a0 b0 a * b
theorem Zsqrtd.not_sqLe_succ (c : ) (d : ) (y : ) (h : 0 < c) :
¬Zsqrtd.SqLe (y + 1) c 0 d

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.Nonsquare.ns (x : ) [] (n : ) :
x n * n
theorem Zsqrtd.d_pos {d : } [dnsq : ] :
0 < d
theorem Zsqrtd.divides_sq_eq_zero {d : } [dnsq : ] {x : } {y : } (h : x * x = d * y * y) :
x = 0 y = 0
theorem Zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : ] {x : } {y : } (h : x * x = d * y * y) :
x = 0 y = 0
theorem Zsqrtd.not_divides_sq {d : } [dnsq : ] (x : ) (y : ) :
(x + 1) * (x + 1) d * (y + 1) * (y + 1)
theorem Zsqrtd.nonneg_antisymm {d : } [dnsq : ] {a : ℤ√d} :
a = 0
theorem Zsqrtd.le_antisymm {d : } [dnsq : ] {a : ℤ√d} {b : ℤ√d} (ab : a b) (ba : b a) :
a = b
instance Zsqrtd.linearOrder {d : } [dnsq : ] :
theorem Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : ] {a : ℤ√d} {b : ℤ√d} :
a * b = 0a = 0 b = 0
theorem Zsqrtd.mul_pos {d : } [dnsq : ] (a : ℤ√d) (b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) :
0 < a * b
theorem Zsqrtd.norm_eq_zero {d : } (h_nonsquare : ∀ (n : ), d n * n) (a : ℤ√d) :
= 0 a = 0
theorem Zsqrtd.hom_ext {R : Type} [Ring R] {d : } (f : ℤ√d →+* R) (g : ℤ√d →+* R) (h : f Zsqrtd.sqrtd = g Zsqrtd.sqrtd) :
f = g
@[simp]
theorem Zsqrtd.lift_apply_apply {R : Type} [] {d : } (r : { r // r * r = d }) (a : ℤ√d) :
↑(Zsqrtd.lift r) a = a.re + a.im * r
@[simp]
theorem Zsqrtd.lift_symm_apply_coe {R : Type} [] {d : } (f : ℤ√d →+* R) :
↑(Zsqrtd.lift.symm f) = f Zsqrtd.sqrtd
def Zsqrtd.lift {R : Type} [] {d : } :
{ r // r * r = d } (ℤ√d →+* R)

The unique RingHom from ℤ√d to a ring R, constructed by replacing √d with the provided root. Conversely, this associates to every mapping ℤ√d →+* R a value of √d in R.

Instances For
theorem Zsqrtd.lift_injective {R : Type} [] [] {d : } (r : { r // r * r = d }) (hd : ∀ (n : ), d n * n) :
Function.Injective ↑(Zsqrtd.lift r)

lift r is injective if d is non-square, and R has characteristic zero (that is, the map from ℤ into R is injective).

An element of ℤ√d has norm equal to 1 if and only if it is contained in the submonoid of unitary elements.

theorem Zsqrtd.mker_norm_eq_unitary {d : } :
MonoidHom.mker Zsqrtd.normMonoidHom = unitary (ℤ√d)

The kernel of the norm map on ℤ√d equals the submonoid of unitary elements.