# mathlib3documentation

number_theory.zsqrtd.basic

# ℤ[√d] #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 `zsqrtd`
@[protected, instance]
def zsqrtd.decidable_eq {d : } :
Equations
theorem zsqrtd.ext {d : } {z w : ℤ√d} :
z = w z.re = w.re z.im = w.im
def zsqrtd.of_int {d : } (n : ) :

Convert an integer to a `ℤ√d`

Equations
theorem zsqrtd.of_int_re {d : } (n : ) :
.re = n
theorem zsqrtd.of_int_im {d : } (n : ) :
.im = 0
@[protected, instance]

The zero of the ring

Equations
@[simp]
theorem zsqrtd.zero_re {d : } :
0.re = 0
@[simp]
theorem zsqrtd.zero_im {d : } :
0.im = 0
@[protected, instance]
Equations
@[protected, instance]
def zsqrtd.has_one {d : } :

The one of the ring

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 : } :
@[protected, instance]
def zsqrtd.has_add {d : } :

Addition of elements of `ℤ√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
@[protected, instance]
def zsqrtd.has_neg {d : } :

Negation in `ℤ√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
@[protected, instance]
def zsqrtd.has_mul {d : } :

Multiplication in `ℤ√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
@[protected, instance]
def zsqrtd.add_comm_group {d : } :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def zsqrtd.monoid {d : } :
Equations
@[protected, instance]
def zsqrtd.comm_monoid {d : } :
Equations
@[protected, instance]
def zsqrtd.comm_semigroup {d : } :
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def zsqrtd.add_semigroup {d : } :
Equations
@[protected, instance]
def zsqrtd.comm_semiring {d : } :
Equations
@[protected, instance]
Equations
@[protected, instance]
def zsqrtd.ring {d : } :
Equations
@[protected, instance]
def zsqrtd.distrib {d : } :
Equations
@[protected, instance]

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

Equations
@[simp]
theorem zsqrtd.star_mk {d : } (x y : ) :
has_star.star {re := x, im := y} = {re := x, im := -y}
@[simp]
theorem zsqrtd.star_re {d : } (z : ℤ√d) :
.re = z.re
@[simp]
theorem zsqrtd.star_im {d : } (z : ℤ√d) :
.im = -z.im
@[protected, instance]
Equations
@[protected, 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}
@[protected, 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}
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 : } :
@[simp]
theorem zsqrtd.smuld_val {d : } (n x y : ) :
* {re := x, im := y} = {re := d * n * y, im := n * x}
theorem zsqrtd.decompose {d x y : } :
{re := x, im := y} = x +
theorem zsqrtd.mul_star {d x y : } :
{re := x, im := y} * has_star.star {re := x, im := y} = x * x - d * y * y
@[protected]
theorem zsqrtd.coe_int_add {d : } (m n : ) :
(m + n) = m + n
@[protected]
theorem zsqrtd.coe_int_sub {d : } (m n : ) :
(m - n) = m - n
@[protected]
theorem zsqrtd.coe_int_mul {d : } (m n : ) :
(m * n) = m * n
@[protected]
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, norm_cast]
theorem zsqrtd.coe_int_dvd_coe_int {d : } (a b : ) :
a b a b
@[protected]
theorem zsqrtd.eq_of_smul_eq_smul_left {d a : } {b c : ℤ√d} (ha : a 0) (h : a * b = a * c) :
b = c
theorem zsqrtd.gcd_eq_zero_iff {d : } (a : ℤ√d) :
a.re.gcd a.im = 0 a = 0
theorem zsqrtd.gcd_pos_iff {d : } (a : ℤ√d) :
0 < a.re.gcd a.im a 0
theorem zsqrtd.coprime_of_dvd_coprime {d : } {a b : ℤ√d} (hcoprime : a.im) (hdvd : b a) :
b.im
theorem zsqrtd.exists_coprime_of_gcd_pos {d : } {a : ℤ√d} (hgcd : 0 < a.re.gcd a.im) :
(b : ℤ√d), a = (a.re.gcd a.im) * b b.im
def zsqrtd.sq_le (a c b d : ) :
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 : } (xz : z x) (yw : y w) (xy : c y d) :
c w d
theorem zsqrtd.sq_le_add_mixed {c d x y z w : } (xy : c y d) (zw : c w d) :
c * (x * z) d * (y * w)
theorem zsqrtd.sq_le_add {c d x y z w : } (xy : c y d) (zw : c w d) :
zsqrtd.sq_le (x + z) c (y + w) d
theorem zsqrtd.sq_le_cancel {c d x y z w : } (zw : d x c) (h : zsqrtd.sq_le (x + z) c (y + w) d) :
c w d
theorem zsqrtd.sq_le_smul {c d x y : } (n : ) (xy : c y d) :
zsqrtd.sq_le (n * x) c (n * y) d
theorem zsqrtd.sq_le_mul {d x y z w : } :
1 y d 1 w d zsqrtd.sq_le (x * w + y * z) d (x * z + d * y * w) 1) 1 y d d z 1 zsqrtd.sq_le (x * z + d * y * w) 1 (x * w + y * z) d) d x 1 1 w d zsqrtd.sq_le (x * z + d * y * w) 1 (x * w + y * z) d) d x 1 d z 1 zsqrtd.sq_le (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

Equations
Instances for `zsqrtd.nonnegg`
theorem zsqrtd.nonnegg_comm {c d : } {x y : } :
x y = y x
theorem zsqrtd.nonnegg_neg_pos {c d a b : } :
(-a) b d b c
theorem zsqrtd.nonnegg_pos_neg {c d a b : } :
a (-b) c a d
theorem zsqrtd.nonnegg_cases_right {c d a : } {b : } :
( (x : ), b = -x c a d) a b
theorem zsqrtd.nonnegg_cases_left {c d b : } {a : } (h : (x : ), a = -x d b c) :
a b
def zsqrtd.norm {d : } (n : ℤ√d) :

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

Equations
theorem zsqrtd.norm_def {d : } (n : ℤ√d) :
n.norm = n.re * n.re - d * n.im * n.im
@[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 : ) :
@[simp]
theorem zsqrtd.norm_mul {d : } (n m : ℤ√d) :
(n * m).norm = n.norm * m.norm

`norm` as a `monoid_hom`.

Equations
theorem zsqrtd.norm_eq_mul_conj {d : } (n : ℤ√d) :
(n.norm) =
@[simp]
theorem zsqrtd.norm_neg {d : } (x : ℤ√d) :
(-x).norm = x.norm
@[simp]
theorem zsqrtd.norm_conj {d : } (x : ℤ√d) :
theorem zsqrtd.norm_nonneg {d : } (hd : d 0) (n : ℤ√d) :
0 n.norm
theorem zsqrtd.norm_eq_one_iff {d : } {x : ℤ√d} :
theorem zsqrtd.norm_eq_one_iff' {d : } (hd : d 0) (z : ℤ√d) :
z.norm = 1
theorem zsqrtd.norm_eq_zero_iff {d : } (hd : d < 0) (z : ℤ√d) :
z.norm = 0 z = 0
theorem zsqrtd.norm_eq_of_associated {d : } (hd : d 0) {x y : ℤ√d} (h : y) :
x.norm = y.norm
def zsqrtd.nonneg {d : } :

Nonnegativity of an element of `ℤ√d`.

Equations
Instances for `zsqrtd.nonneg`
@[protected, instance]
def zsqrtd.has_le {d : } :
Equations
@[protected, instance]
def zsqrtd.has_lt {d : } :
Equations
@[protected, instance]
def zsqrtd.decidable_nonnegg (c d : ) (a b : ) :
decidable d a b)
Equations
@[protected, instance]
def zsqrtd.decidable_nonneg {d : } (a : ℤ√d) :
Equations
@[protected, instance]
def zsqrtd.decidable_le {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 : } (xy : {re := x, im := -y}.nonneg) (zw : {re := -z, im := w}.nonneg) :
({re := x, im := -y} + {re := -z, im := w}).nonneg
theorem zsqrtd.nonneg.add {d : } {a b : ℤ√d} (ha : a.nonneg) (hb : b.nonneg) :
(a + b).nonneg
theorem zsqrtd.nonneg_iff_zero_le {d : } {a : ℤ√d} :
a.nonneg 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}
@[protected]
theorem zsqrtd.nonneg_total {d : } (a : ℤ√d) :
@[protected]
theorem zsqrtd.le_total {d : } (a b : ℤ√d) :
a b b a
@[protected, instance]
Equations
theorem zsqrtd.le_arch {d : } (a : ℤ√d) :
(n : ), a n
@[protected]
theorem zsqrtd.add_le_add_left {d : } (a b : ℤ√d) (ab : a b) (c : ℤ√d) :
c + a c + b
@[protected]
theorem zsqrtd.le_of_add_le_add_left {d : } (a b c : ℤ√d) (h : c + a c + b) :
a b
@[protected]
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 : } (ha : a.nonneg) :
(n * a).nonneg
theorem zsqrtd.nonneg_muld {d : } {a : ℤ√d} (ha : a.nonneg) :
theorem zsqrtd.nonneg_mul_lem {d x y : } {a : ℤ√d} (ha : a.nonneg) :
({re := x, im := y} * a).nonneg
theorem zsqrtd.nonneg_mul {d : } {a b : ℤ√d} (ha : a.nonneg) (hb : b.nonneg) :
(a * b).nonneg
@[protected]
theorem zsqrtd.mul_nonneg {d : } (a b : ℤ√d) :
0 a 0 b 0 a * b
theorem zsqrtd.not_sq_le_succ (c d y : ) (h : 0 < c) :
¬zsqrtd.sq_le (y + 1) c 0 d
@[class]
structure zsqrtd.nonsquare (x : ) :
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 of this typeclass
theorem zsqrtd.d_pos {d : } [dnsq : zsqrtd.nonsquare d] :
0 < d
theorem zsqrtd.divides_sq_eq_zero {d : } [dnsq : zsqrtd.nonsquare d] {x y : } (h : x * x = d * y * y) :
x = 0 y = 0
theorem zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : zsqrtd.nonsquare d] {x y : } (h : x * x = d * y * y) :
x = 0 y = 0
theorem zsqrtd.not_divides_sq {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).nonneg a = 0
theorem zsqrtd.le_antisymm {d : } [dnsq : zsqrtd.nonsquare d] {a b : ℤ√d} (ab : a b) (ba : b a) :
a = b
@[protected, instance]
def zsqrtd.linear_order {d : } [dnsq : zsqrtd.nonsquare d] :
Equations
@[protected]
theorem zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : zsqrtd.nonsquare d] {a b : ℤ√d} :
a * b = 0 a = 0 b = 0
@[protected, instance]
def zsqrtd.no_zero_divisors {d : } [dnsq : zsqrtd.nonsquare d] :
@[protected, instance]
@[protected]
theorem zsqrtd.mul_pos {d : } [dnsq : zsqrtd.nonsquare d] (a b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) :
0 < a * b
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
def zsqrtd.ordered_ring {d : } [dnsq : zsqrtd.nonsquare d] :
Equations
theorem zsqrtd.norm_eq_zero {d : } (h_nonsquare : (n : ), d n * n) (a : ℤ√d) :
a.norm = 0 a = 0
@[ext]
theorem zsqrtd.hom_ext {R : Type} [ring R] {d : } (f g : ℤ√d →+* R) (h : = ) :
f = g
@[simp]
theorem zsqrtd.lift_symm_apply_coe {R : Type} [comm_ring R] {d : } (f : ℤ√d →+* R) :
@[simp]
theorem zsqrtd.lift_apply_apply {R : Type} [comm_ring R] {d : } (r : {r // r * r = d}) (a : ℤ√d) :
def zsqrtd.lift {R : Type} [comm_ring R] {d : } :
{r // r * r = d} (ℤ√d →+* R)

The unique `ring_hom` 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`.

Equations
theorem zsqrtd.lift_injective {R : Type} [comm_ring R] [char_zero R] {d : } (r : {r // r * r = d}) (hd : (n : ), d n * n) :

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

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