ℤ[√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 : ℤ) : 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.

• re : ℤ

  Component of the integer not multiplied by √d

• im : ℤ

  Component of the integer multiplied by √d

theorem Zsqrtd.ext_iff {d : ℤ} {x y : ℤ√d} : x = y ↔ x.re = y.re ∧ x.im = y.im

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

instance instDecidableEqZsqrtd {d✝ : ℤ} : DecidableEq (ℤ√d✝)

def «termℤ√_» : Lean.ParserDescr

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.

def Zsqrtd.ofInt {d : ℤ} (n : ℤ) : ℤ√d

Convert an integer to a ℤ√d

theorem Zsqrtd.ofInt_re {d : ℤ} (n : ℤ) : (ofInt n).re = n

theorem Zsqrtd.ofInt_im {d : ℤ} (n : ℤ) : (ofInt n).im = 0

instance Zsqrtd.instZero {d : ℤ} : Zero (ℤ√d)

The zero of the ring

@[simp]

theorem Zsqrtd.zero_re {d : ℤ} : re 0 = 0

@[simp]

theorem Zsqrtd.zero_im {d : ℤ} : im 0 = 0

instance Zsqrtd.instInhabited {d : ℤ} : Inhabited (ℤ√d)

instance Zsqrtd.instOne {d : ℤ} : One (ℤ√d)

The one of the ring

@[simp]

theorem Zsqrtd.one_re {d : ℤ} : re 1 = 1

@[simp]

theorem Zsqrtd.one_im {d : ℤ} : im 1 = 0

def Zsqrtd.sqrtd {d : ℤ} : ℤ√d

The representative of √d in the ring

@[simp]

theorem Zsqrtd.sqrtd_re {d : ℤ} : sqrtd.re = 0

@[simp]

theorem Zsqrtd.sqrtd_im {d : ℤ} : sqrtd.im = 1

instance Zsqrtd.instAdd {d : ℤ} : Add (ℤ√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 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 : ℤ} : Neg (ℤ√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.instMul {d : ℤ} : Mul (ℤ√d)

Multiplication in ℤ√d

@[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 Zsqrtd.addCommGroup {d : ℤ} : AddCommGroup (ℤ√d)

@[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.addGroupWithOne {d : ℤ} : AddGroupWithOne (ℤ√d)

instance Zsqrtd.commRing {d : ℤ} : CommRing (ℤ√d)

instance Zsqrtd.instAddMonoid {d : ℤ} : AddMonoid (ℤ√d)

instance Zsqrtd.instMonoid {d : ℤ} : Monoid (ℤ√d)

instance Zsqrtd.instCommMonoid {d : ℤ} : CommMonoid (ℤ√d)

instance Zsqrtd.instCommSemigroup {d : ℤ} : CommSemigroup (ℤ√d)

instance Zsqrtd.instSemigroup {d : ℤ} : Semigroup (ℤ√d)

instance Zsqrtd.instAddCommSemigroup {d : ℤ} : AddCommSemigroup (ℤ√d)

instance Zsqrtd.instAddSemigroup {d : ℤ} : AddSemigroup (ℤ√d)

instance Zsqrtd.instCommSemiring {d : ℤ} : CommSemiring (ℤ√d)

instance Zsqrtd.instSemiring {d : ℤ} : Semiring (ℤ√d)

instance Zsqrtd.instRing {d : ℤ} : Ring (ℤ√d)

instance Zsqrtd.instDistrib {d : ℤ} : Distrib (ℤ√d)

instance Zsqrtd.instStar {d : ℤ} : Star (ℤ√d)

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

instance Zsqrtd.instStarRing {d : ℤ} : StarRing (ℤ√d)

instance Zsqrtd.nontrivial {d : ℤ} : Nontrivial (ℤ√d)

@[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] : (OfNat.ofNat n).im = 0

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 }

instance Zsqrtd.instCharZero {d : ℤ} : CharZero (ℤ√d)

@[simp]

theorem Zsqrtd.ofInt_eq_intCast {d : ℤ} (n : ℤ) : ofInt n = ↑n

@[simp]

theorem Zsqrtd.nsmul_val {d : ℤ} (n : ℕ) (x y : ℤ) : ↑n * { re := x, im := y } = { re := ↑n * x, im := ↑n * y }

@[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) : IsCoprime b.re b.im

@[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) : IsCoprime b.re b.im

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

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

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 d → SqLe z 1 w d → SqLe (x * w + y * z) d (x * z + d * y * w) 1) ∧ (SqLe x 1 y d → SqLe w d z 1 → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧ (SqLe y d x 1 → SqLe z 1 w d → SqLe (x * z + d * y * w) 1 (x * w + y * z) d) ∧ (SqLe y d x 1 → SqLe w d z 1 → 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

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 = -↑x → SqLe x c a d) → Nonnegg c d (↑a) b

theorem Zsqrtd.nonnegg_cases_left {c d b : ℕ} {a : ℤ} (h : ∀ (x : ℕ), a = -↑x → SqLe x d b c) : Nonnegg c d a ↑b

def Zsqrtd.norm {d : ℤ} (n : ℤ√d) : ℤ

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

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

def Zsqrtd.normMonoidHom {d : ℤ} : ℤ√d →* ℤ

norm as a MonoidHom.

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

@[simp]

theorem Zsqrtd.abs_norm {d : ℤ} (hd : d ≤ 0) (n : ℤ√d) : |n.norm| = n.norm

theorem Zsqrtd.norm_eq_one_iff {d : ℤ} {x : ℤ√d} : x.norm.natAbs = 1 ↔ IsUnit x

theorem Zsqrtd.isUnit_iff_norm_isUnit {d : ℤ} (z : ℤ√d) : IsUnit z ↔ IsUnit z.norm

theorem Zsqrtd.norm_eq_one_iff' {d : ℤ} (hd : d ≤ 0) (z : ℤ√d) : z.norm = 1 ↔ IsUnit z

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 : ℕ} : ℤ√↑d → Prop

Nonnegativity of an element of ℤ√d.

instance Zsqrtd.instLECastInt {d : ℕ} : LE (ℤ√↑d)

instance Zsqrtd.instLTCastInt {d : ℕ} : LT (ℤ√↑d)

instance Zsqrtd.decidableNonnegg (c d : ℕ) (a b : ℤ) : Decidable (Nonnegg c d a b)

instance Zsqrtd.decidableNonneg {d : ℕ} (a : ℤ√↑d) : Decidable a.Nonneg

instance Zsqrtd.decidableLE {d : ℕ} : DecidableLE (ℤ√↑d)

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) : a.Nonneg ∨ (-a).Nonneg

theorem Zsqrtd.le_total {d : ℕ} (a b : ℤ√↑d) : a ≤ b ∨ b ≤ a

instance Zsqrtd.preorder {d : ℕ} : Preorder (ℤ√↑d)

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) : (sqrtd * 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 ≤ a → 0 ≤ b → 0 ≤ a * b

theorem Zsqrtd.not_sqLe_succ (c d y : ℕ) (h : 0 < c) : ¬SqLe (y + 1) c 0 d

class 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.

• ns' (n : ℕ) : x ≠ n * n

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).Nonneg → a = 0

theorem Zsqrtd.le_antisymm {d : ℕ} [dnsq : Nonsquare d] {a b : ℤ√↑d} (ab : a ≤ b) (ba : b ≤ a) : a = b

instance Zsqrtd.linearOrder {d : ℕ} [dnsq : Nonsquare d] : LinearOrder (ℤ√↑d)

theorem Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : ℕ} [dnsq : Nonsquare d] {a b : ℤ√↑d} : a * b = 0 → a = 0 ∨ b = 0

instance Zsqrtd.instNoZeroDivisorsCastInt {d : ℕ} [dnsq : Nonsquare d] : NoZeroDivisors (ℤ√↑d)

instance Zsqrtd.instIsDomainCastInt {d : ℕ} [dnsq : Nonsquare d] : IsDomain (ℤ√↑d)

theorem Zsqrtd.mul_pos {d : ℕ} [dnsq : Nonsquare d] (a b : ℤ√↑d) (a0 : 0 < a) (b0 : 0 < b) : 0 < a * b

instance Zsqrtd.instZeroLEOneClassCastInt {d : ℕ} : ZeroLEOneClass (ℤ√↑d)

instance Zsqrtd.instIsOrderedAddMonoidCastInt {d : ℕ} [dnsq : Nonsquare d] : IsOrderedAddMonoid (ℤ√↑d)

instance Zsqrtd.instIsStrictOrderedRingCastInt {d : ℕ} [dnsq : Nonsquare d] : IsStrictOrderedRing (ℤ√↑d)

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} [NonAssocRing R] {d : ℤ} (f g : ℤ√d →+* R) (h : f sqrtd = g sqrtd) : f = g

theorem Zsqrtd.hom_ext_iff {R : Type} [NonAssocRing R] {d : ℤ} {f g : ℤ√d →+* R} : f = g ↔ f sqrtd = g sqrtd

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.

@[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) : Function.Injective ⇑(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).

theorem Zsqrtd.norm_eq_one_iff_mem_unitary {d : ℤ} {a : ℤ√d} : a.norm = 1 ↔ a ∈ unitary (ℤ√d)

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 normMonoidHom = unitary (ℤ√d)

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