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.

  • re :

    Component of the integer not multiplied by √d

  • im :

    Component of the integer multiplied by √d

theorem Zsqrtd.ext {d : } {x y : ℤ√d} (re : x.re = y.re) (im : x.im = y.im) :
x = y

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.

Equations
def Zsqrtd.ofInt {d : } (n : ) :

Convert an integer to a ℤ√d

Equations
theorem Zsqrtd.ofInt_re {d : } (n : ) :
(ofInt n).re = n
theorem Zsqrtd.ofInt_im {d : } (n : ) :
(ofInt n).im = 0
instance Zsqrtd.instZero {d : } :

The zero of the ring

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

The one of the ring

Equations
@[simp]
theorem Zsqrtd.one_re {d : } :
re 1 = 1
@[simp]
theorem Zsqrtd.one_im {d : } :
im 1 = 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 : } :
instance Zsqrtd.instAdd {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
instance Zsqrtd.instNeg {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
instance Zsqrtd.instMul {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
@[simp]
theorem Zsqrtd.sub_re {d : } (z w : ℤ√d) :
(z - w).re = z.re - w.re
@[simp]
theorem Zsqrtd.sub_im {d : } (z w : ℤ√d) :
(z - w).im = z.im - w.im
instance Zsqrtd.instStar {d : } :

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

Equations
@[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.natCast_re {d : } (n : ) :
(↑n).re = n
@[simp]
theorem Zsqrtd.ofNat_re {d : } (n : ) [n.AtLeastTwo] :
(OfNat.ofNat n).re = n
@[simp]
theorem Zsqrtd.natCast_im {d : } (n : ) :
(↑n).im = 0
@[simp]
theorem Zsqrtd.ofNat_im {d : } (n : ) [n.AtLeastTwo] :
theorem Zsqrtd.natCast_val {d : } (n : ) :
n = { re := n, im := 0 }
@[simp]
theorem Zsqrtd.intCast_re {d : } (n : ) :
(↑n).re = n
@[simp]
theorem Zsqrtd.intCast_im {d : } (n : ) :
(↑n).im = 0
theorem Zsqrtd.intCast_val {d : } (n : ) :
n = { re := n, im := 0 }
@[simp]
theorem Zsqrtd.ofInt_eq_intCast {d : } (n : ) :
ofInt 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 : ) :
sqrtd * { re := x, im := y } = { re := d * y, im := x }
@[simp]
theorem Zsqrtd.dmuld {d : } :
sqrtd * sqrtd = d
@[simp]
theorem Zsqrtd.smuld_val {d : } (n x y : ) :
sqrtd * n * { re := x, im := y } = { re := d * n * y, im := n * x }
theorem Zsqrtd.decompose {d x y : } :
{ re := x, im := y } = x + 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.intCast_dvd {d : } (z : ) (a : ℤ√d) :
z a z a.re z a.im
@[simp]
theorem Zsqrtd.intCast_dvd_intCast {d : } (a b : ) :
a b a b
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.isCoprime_of_dvd_isCoprime {d : } {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b a) :
@[deprecated Zsqrtd.isCoprime_of_dvd_isCoprime (since := "2025-01-23")]
theorem Zsqrtd.coprime_of_dvd_coprime {d : } {a b : ℤ√d} (hcoprime : IsCoprime a.re a.im) (hdvd : b a) :

Alias of Zsqrtd.isCoprime_of_dvd_isCoprime.

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 IsCoprime b.re b.im
def Zsqrtd.SqLe (a c b d : ) :

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

Equations
theorem Zsqrtd.sqLe_of_le {c d x y z w : } (xz : z x) (yw : y w) (xy : SqLe x c y d) :
SqLe z c w d
theorem Zsqrtd.sqLe_add_mixed {c d x y z w : } (xy : SqLe x c y d) (zw : SqLe z c w d) :
c * (x * z) d * (y * w)
theorem Zsqrtd.sqLe_add {c d x y z w : } (xy : SqLe x c y d) (zw : SqLe z c w d) :
SqLe (x + z) c (y + w) d
theorem Zsqrtd.sqLe_cancel {c d x y z w : } (zw : SqLe y d x c) (h : SqLe (x + z) c (y + w) d) :
SqLe z c w d
theorem Zsqrtd.sqLe_smul {c d x y : } (n : ) (xy : SqLe x c y d) :
SqLe (n * x) c (n * y) d
theorem Zsqrtd.sqLe_mul {d x y z w : } :
(SqLe x 1 y dSqLe z 1 w dSqLe (x * w + y * z) d (x * z + d * y * w) 1) (SqLe x 1 y dSqLe w d z 1SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (SqLe y d x 1SqLe z 1 w dSqLe (x * z + d * y * w) 1 (x * w + y * z) d) (SqLe y d x 1SqLe w d z 1SqLe (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
theorem Zsqrtd.nonnegg_comm {c d : } {x y : } :
Nonnegg c d x y = Nonnegg d c y x
theorem Zsqrtd.nonnegg_neg_pos {c d a b : } :
Nonnegg c d (-a) b SqLe a d b c
theorem Zsqrtd.nonnegg_pos_neg {c d a b : } :
Nonnegg c d (↑a) (-b) SqLe b c a d
theorem Zsqrtd.nonnegg_cases_right {c d a : } {b : } :
(∀ (x : ), b = -xSqLe x c a d)Nonnegg c d (↑a) b
theorem Zsqrtd.nonnegg_cases_left {c d b : } {a : } (h : ∀ (x : ), a = -xSqLe x d b c) :
Nonnegg c d 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 : } :
norm 0 = 0
@[simp]
theorem Zsqrtd.norm_one {d : } :
norm 1 = 1
@[simp]
theorem Zsqrtd.norm_intCast {d : } (n : ) :
(↑n).norm = n * n
@[simp]
theorem Zsqrtd.norm_natCast {d : } (n : ) :
(↑n).norm = n * n
@[simp]
theorem Zsqrtd.norm_mul {d : } (n m : ℤ√d) :
(n * m).norm = n.norm * m.norm

norm as a MonoidHom.

Equations
theorem Zsqrtd.norm_eq_mul_conj {d : } (n : ℤ√d) :
n.norm = n * star n
@[simp]
theorem Zsqrtd.norm_neg {d : } (x : ℤ√d) :
(-x).norm = x.norm
@[simp]
theorem Zsqrtd.norm_conj {d : } (x : ℤ√d) :
(star x).norm = x.norm
theorem Zsqrtd.norm_nonneg {d : } (hd : d 0) (n : ℤ√d) :
0 n.norm
theorem Zsqrtd.norm_eq_one_iff' {d : } (hd : d 0) (z : ℤ√d) :
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 : Associated x y) :
x.norm = y.norm
def Zsqrtd.Nonneg {d : } :
ℤ√dProp

Nonnegativity of an element of ℤ√d.

Equations
instance Zsqrtd.instLECastInt {d : } :
LE (ℤ√d)
Equations
instance Zsqrtd.instLTCastInt {d : } :
LT (ℤ√d)
Equations
instance Zsqrtd.decidableNonnegg (c d : ) (a b : ) :
Decidable (Nonnegg c d a b)
Equations
  • One or more equations did not get rendered due to their size.
instance Zsqrtd.decidableNonneg {d : } (a : ℤ√d) :
Equations
instance Zsqrtd.decidableLE {d : } :
DecidableRel fun (x1 x2 : ℤ√d) => x1 x2
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 }
theorem Zsqrtd.nonneg_total {d : } (a : ℤ√d) :
theorem Zsqrtd.le_total {d : } (a b : ℤ√d) :
a b b a
instance Zsqrtd.preorder {d : } :
Equations
theorem Zsqrtd.le_arch {d : } (a : ℤ√d) :
∃ (n : ), a n
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) (h : c + a c + b) :
a 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 : } (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
theorem Zsqrtd.mul_nonneg {d : } (a b : ℤ√d) :
0 a0 b0 a * b
theorem Zsqrtd.not_sqLe_succ (c d y : ) (h : 0 < c) :
¬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 : ) [Nonsquare x] (n : ) :
    x n * n
    theorem Zsqrtd.d_pos {d : } [dnsq : Nonsquare d] :
    0 < d
    theorem Zsqrtd.divides_sq_eq_zero {d : } [dnsq : Nonsquare d] {x y : } (h : x * x = d * y * y) :
    x = 0 y = 0
    theorem Zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : Nonsquare d] {x y : } (h : x * x = d * y * y) :
    x = 0 y = 0
    theorem Zsqrtd.not_divides_sq {d : } [dnsq : Nonsquare d] (x y : ) :
    (x + 1) * (x + 1) d * (y + 1) * (y + 1)
    theorem Zsqrtd.nonneg_antisymm {d : } [dnsq : Nonsquare d] {a : ℤ√d} :
    a.Nonneg(-a).Nonnega = 0
    theorem Zsqrtd.le_antisymm {d : } [dnsq : Nonsquare d] {a b : ℤ√d} (ab : a b) (ba : b a) :
    a = b
    theorem Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : Nonsquare d] {a b : ℤ√d} :
    a * b = 0a = 0 b = 0
    theorem Zsqrtd.mul_pos {d : } [dnsq : Nonsquare d] (a 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) :
    a.norm = 0 a = 0
    theorem Zsqrtd.hom_ext {R : Type} [Ring R] {d : } (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) :
    f = g
    def Zsqrtd.lift {R : Type} [CommRing R] {d : } :
    { r : 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.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem Zsqrtd.lift_symm_apply_coe {R : Type} [CommRing R] {d : } (f : ℤ√d →+* R) :
    (lift.symm f) = f sqrtd
    @[simp]
    theorem Zsqrtd.lift_apply_apply {R : Type} [CommRing R] {d : } (r : { r : R // r * r = d }) (a : ℤ√d) :
    (lift r) a = a.re + a.im * r
    theorem Zsqrtd.lift_injective {R : Type} [CommRing R] [CharZero R] {d : } (r : { 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.

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