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

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

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

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 : ℤ
• im : ℤ

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

Equations

• instDecidableEqZsqrtd = decEqZsqrtd✝

def «termℤ√_» : Lean.ParserDescr

Equations

• «termℤ√_» = Lean.ParserDescr.node `termℤ√_ 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ℤ√") (Lean.ParserDescr.cat `term 100))

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

Convert an integer to a ℤ√d

Equations

• Zsqrtd.ofInt n = { re := n, im := 0 }

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

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

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

The zero of the ring

Equations

• Zsqrtd.instZeroZsqrtd = { zero := Zsqrtd.ofInt 0 }

@[simp]

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

@[simp]

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

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

Equations

• Zsqrtd.instInhabitedZsqrtd = { default := 0 }

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

The one of the ring

Equations

• Zsqrtd.instOneZsqrtd = { one := Zsqrtd.ofInt 1 }

@[simp]

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

@[simp]

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

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

The representative of √d in the ring

Equations

• Zsqrtd.sqrtd = { re := 0, im := 1 }

@[simp]

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

@[simp]

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

instance Zsqrtd.instAddZsqrtd {d : ℤ} : Add (ℤ√d)

Addition of elements of ℤ√d

Equations

• Zsqrtd.instAddZsqrtd = { add := fun (z w : ℤ√d) => { re := z.re + w.re, im := z.im + w.im } }

@[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 : ℤ} : Neg (ℤ√d)

Negation in ℤ√d

Equations

• Zsqrtd.instNegZsqrtd = { neg := fun (z : ℤ√d) => { re := -z.re, im := -z.im } }

@[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 : ℤ} : Mul (ℤ√d)

Multiplication in ℤ√d

Equations

• Zsqrtd.instMulZsqrtd = { mul := fun (z w : ℤ√d) => { re := z.re * w.re + d * z.im * w.im, im := z.re * w.im + z.im * w.re } }

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

instance Zsqrtd.addCommGroup {d : ℤ} : AddCommGroup (ℤ√d)

Equations

• Zsqrtd.addCommGroup = AddCommGroup.mk (_ : ∀ (a b : ℤ√d), a + b = b + a)

@[simp]

theorem Zsqrtd.sub_re {d : ℤ} (z : ℤ√d) (w : ℤ√d) : (z - w).re = z.re - w.re

@[simp]

theorem Zsqrtd.sub_im {d : ℤ} (z : ℤ√d) (w : ℤ√d) : (z - w).im = z.im - w.im

instance Zsqrtd.addGroupWithOne {d : ℤ} : AddGroupWithOne (ℤ√d)

Equations

• Zsqrtd.addGroupWithOne = let src := Zsqrtd.addCommGroup; AddGroupWithOne.mk SubNegMonoid.zsmul (_ : ∀ (a : ℤ√d), -a + a = 0)

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

Equations

• Zsqrtd.commRing = let src := Zsqrtd.addGroupWithOne; CommRing.mk (_ : ∀ (a b : ℤ√d), a * b = b * a)

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

Equations

• Zsqrtd.instAddMonoidZsqrtd = inferInstance

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

Equations

• Zsqrtd.instMonoidZsqrtd = inferInstance

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

Equations

• Zsqrtd.instCommMonoidZsqrtd = inferInstance

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

Equations

• Zsqrtd.instCommSemigroupZsqrtd = inferInstance

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

Equations

• Zsqrtd.instSemigroupZsqrtd = inferInstance

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

Equations

• Zsqrtd.instAddCommSemigroupZsqrtd = inferInstance

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

Equations

• Zsqrtd.instAddSemigroupZsqrtd = inferInstance

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

Equations

• Zsqrtd.instCommSemiringZsqrtd = inferInstance

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

Equations

• Zsqrtd.instSemiringZsqrtd = inferInstance

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

Equations

• Zsqrtd.instRingZsqrtd = inferInstance

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

Equations

• Zsqrtd.instDistribZsqrtd = inferInstance

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

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

Equations

• Zsqrtd.instStarZsqrtd = { star := fun (z : ℤ√d) => { re := z.re, im := -z.im } }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• (_ : Nontrivial (ℤ√d)) = (_ : Nontrivial (ℤ√d))

@[simp]

theorem Zsqrtd.coe_nat_re {d : ℤ} (n : ℕ) : (↑n).re = ↑n

@[simp]

theorem Zsqrtd.ofNat_re {d : ℤ} (n : ℕ) [Nat.AtLeastTwo n] : (OfNat.ofNat n).re = ↑n

@[simp]

theorem Zsqrtd.coe_nat_im {d : ℤ} (n : ℕ) : (↑n).im = 0

@[simp]

theorem Zsqrtd.ofNat_im {d : ℤ} (n : ℕ) [Nat.AtLeastTwo n] : (OfNat.ofNat 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 Zsqrtd.instCharZeroZsqrtdToAddMonoidWithOneAddGroupWithOne {d : ℤ} : CharZero (ℤ√d)

Equations

• (_ : CharZero (ℤ√d)) = (_ : CharZero (ℤ√d))

@[simp]

theorem Zsqrtd.ofInt_eq_coe {d : ℤ} (n : ℤ) : Zsqrtd.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 : ℤ) : 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 : ℤ√d), a = ↑↑(Int.gcd a.re 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

Equations

• Zsqrtd.SqLe a c b d = (c * a * a ≤ d * b * b)

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

Equations

• One or more equations did not get rendered due to their size.

theorem Zsqrtd.nonnegg_comm {c : ℕ} {d : ℕ} {x : ℤ} {y : ℤ} : Zsqrtd.Nonnegg c d x y = Zsqrtd.Nonnegg d c y x

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

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

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

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

Equations

• Zsqrtd.norm n = n.re * n.re - d * n.im * n.im

theorem Zsqrtd.norm_def {d : ℤ} (n : ℤ√d) : Zsqrtd.norm n = n.re * n.re - d * n.im * n.im

@[simp]

theorem Zsqrtd.norm_zero {d : ℤ} : Zsqrtd.norm 0 = 0

@[simp]

theorem Zsqrtd.norm_one {d : ℤ} : Zsqrtd.norm 1 = 1

@[simp]

theorem Zsqrtd.norm_int_cast {d : ℤ} (n : ℤ) : Zsqrtd.norm ↑n = n * n

@[simp]

theorem Zsqrtd.norm_nat_cast {d : ℤ} (n : ℕ) : Zsqrtd.norm ↑n = ↑n * ↑n

@[simp]

theorem Zsqrtd.norm_mul {d : ℤ} (n : ℤ√d) (m : ℤ√d) : Zsqrtd.norm (n * m) = Zsqrtd.norm n * Zsqrtd.norm m

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

norm as a MonoidHom.

Equations

• Zsqrtd.normMonoidHom = { toOneHom := { toFun := Zsqrtd.norm, map_one' := (_ : Zsqrtd.norm 1 = 1) }, map_mul' := (_ : ∀ (n m : ℤ√d), Zsqrtd.norm (n * m) = Zsqrtd.norm n * Zsqrtd.norm m) }

theorem Zsqrtd.norm_eq_mul_conj {d : ℤ} (n : ℤ√d) : ↑(Zsqrtd.norm n) = n * star n

@[simp]

theorem Zsqrtd.norm_neg {d : ℤ} (x : ℤ√d) : Zsqrtd.norm (-x) = Zsqrtd.norm x

@[simp]

theorem Zsqrtd.norm_conj {d : ℤ} (x : ℤ√d) : Zsqrtd.norm (star x) = Zsqrtd.norm x

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

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

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

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

theorem Zsqrtd.norm_eq_zero_iff {d : ℤ} (hd : d < 0) (z : ℤ√d) : Zsqrtd.norm z = 0 ↔ z = 0

theorem Zsqrtd.norm_eq_of_associated {d : ℤ} (hd : d ≤ 0) {x : ℤ√d} {y : ℤ√d} (h : Associated x y) : Zsqrtd.norm x = Zsqrtd.norm y

def Zsqrtd.Nonneg {d : ℕ} : ℤ√↑d → Prop

Nonnegativity of an element of ℤ√d.

Equations

• Zsqrtd.Nonneg x = match x with | { re := a, im := b } => Zsqrtd.Nonnegg d 1 a b

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

Equations

• Zsqrtd.instLEZsqrtdCastIntInstNatCastInt = { le := fun (a b : ℤ√↑d) => Zsqrtd.Nonneg (b - a) }

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

Equations

• Zsqrtd.instLTZsqrtdCastIntInstNatCastInt = { lt := fun (a b : ℤ√↑d) => ¬b ≤ a }

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Zsqrtd.decidableNonneg x = match x with | { re := re, im := im } => Zsqrtd.decidableNonnegg d 1 re im

instance Zsqrtd.decidableLE {d : ℕ} : DecidableRel fun (x x_1 : ℤ√↑d) => x ≤ x_1

Equations

• Zsqrtd.decidableLE x✝ x = Zsqrtd.decidableNonneg (x - x✝)

theorem Zsqrtd.nonneg_cases {d : ℕ} {a : ℤ√↑d} : Zsqrtd.Nonneg a → ∃ (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 : Zsqrtd.Nonneg a) (hb : Zsqrtd.Nonneg b) : Zsqrtd.Nonneg (a + b)

theorem Zsqrtd.nonneg_iff_zero_le {d : ℕ} {a : ℤ√↑d} : Zsqrtd.Nonneg a ↔ 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) : Zsqrtd.Nonneg a ∨ Zsqrtd.Nonneg (-a)

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

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

Equations

• Zsqrtd.preorder = Preorder.mk (_ : ∀ (a : ℤ√↑d), Zsqrtd.Nonneg (a - a)) (_ : ∀ (a b c : ℤ√↑d), a ≤ b → b ≤ c → a ≤ c)

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 a) : Zsqrtd.Nonneg (↑n * a)

theorem Zsqrtd.nonneg_muld {d : ℕ} {a : ℤ√↑d} (ha : Zsqrtd.Nonneg a) : Zsqrtd.Nonneg (Zsqrtd.sqrtd * a)

theorem Zsqrtd.nonneg_mul_lem {d : ℕ} {x : ℕ} {y : ℕ} {a : ℤ√↑d} (ha : Zsqrtd.Nonneg a) : Zsqrtd.Nonneg ({ re := ↑x, im := ↑y } * a)

theorem Zsqrtd.nonneg_mul {d : ℕ} {a : ℤ√↑d} {b : ℤ√↑d} (ha : Zsqrtd.Nonneg a) (hb : Zsqrtd.Nonneg b) : Zsqrtd.Nonneg (a * b)

theorem Zsqrtd.mul_nonneg {d : ℕ} (a : ℤ√↑d) (b : ℤ√↑d) : 0 ≤ a → 0 ≤ b → 0 ≤ a * b

theorem Zsqrtd.not_sqLe_succ (c : ℕ) (d : ℕ) (y : ℕ) (h : 0 < c) : ¬Zsqrtd.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 : ℕ) [Zsqrtd.Nonsquare x] (n : ℕ) : x ≠ n * n

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} : Zsqrtd.Nonneg a → Zsqrtd.Nonneg (-a) → a = 0

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

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

Equations

• Zsqrtd.linearOrder = let src := Zsqrtd.preorder; LinearOrder.mk (_ : ∀ (a b : ℤ√↑d), a ≤ b ∨ b ≤ a) Zsqrtd.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE

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

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

Equations

• (_ : NoZeroDivisors (ℤ√↑d)) = (_ : NoZeroDivisors (ℤ√↑d))

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

Equations

• (_ : IsDomain (ℤ√↑d)) = (_ : IsDomain (ℤ√↑d))

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Zsqrtd.instLinearOrderedRingZsqrtdCastIntInstNatCastInt = inferInstance

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

Equations

• Zsqrtd.instOrderedRingZsqrtdCastIntInstNatCastInt = inferInstance

theorem Zsqrtd.norm_eq_zero {d : ℤ} (h_nonsquare : ∀ (n : ℤ), d ≠ n * n) (a : ℤ√d) : Zsqrtd.norm a = 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_symm_apply_coe {R : Type} [CommRing R] {d : ℤ} (f : ℤ√d →+* R) : ↑(Zsqrtd.lift.symm f) = f Zsqrtd.sqrtd

@[simp]

theorem Zsqrtd.lift_apply_apply {R : Type} [CommRing R] {d : ℤ} (r : { r : R // r * r = ↑d }) (a : ℤ√d) : (Zsqrtd.lift r) a = ↑a.re + ↑a.im * ↑r

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.

theorem Zsqrtd.lift_injective {R : Type} [CommRing R] [CharZero R] {d : ℤ} (r : { 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).

theorem Zsqrtd.norm_eq_one_iff_mem_unitary {d : ℤ} {a : ℤ√d} : Zsqrtd.norm a = 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 Zsqrtd.normMonoidHom = unitary (ℤ√d)

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