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

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.instZero {d : ℤ} : Zero (ℤ√d)

The zero of the ring

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• Zsqrtd.instInhabited = { default := 0 }

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

The one of the ring

Equations

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

@[simp]

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

@[simp]

theorem Zsqrtd.one_im {d : ℤ} : Zsqrtd.im 1 = 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.instAdd {d : ℤ} : Add (ℤ√d)

Addition of elements of ℤ√d

Equations

• Zsqrtd.instAdd = { 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 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

Equations

• Zsqrtd.instNeg = { 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.instMul {d : ℤ} : Mul (ℤ√d)

Multiplication in ℤ√d

Equations

• Zsqrtd.instMul = { 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 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)

Equations

• Zsqrtd.addCommGroup = AddCommGroup.mk ⋯

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

Equations

• Zsqrtd.addGroupWithOne = AddGroupWithOne.mk ⋯ SubNegMonoid.zsmul ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

Equations

• Zsqrtd.commRing = CommRing.mk ⋯

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

Equations

• Zsqrtd.instAddMonoid = inferInstance

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

Equations

• Zsqrtd.instMonoid = inferInstance

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

Equations

• Zsqrtd.instCommMonoid = inferInstance

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

Equations

• Zsqrtd.instCommSemigroup = inferInstance

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

Equations

• Zsqrtd.instSemigroup = inferInstance

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

Equations

• Zsqrtd.instAddCommSemigroup = inferInstance

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

Equations

• Zsqrtd.instAddSemigroup = inferInstance

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

Equations

• Zsqrtd.instCommSemiring = inferInstance

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

Equations

• Zsqrtd.instSemiring = inferInstance

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

Equations

• Zsqrtd.instRing = inferInstance

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

Equations

• Zsqrtd.instDistrib = inferInstance

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

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

Equations

• Zsqrtd.instStar = { 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.instStarRing {d : ℤ} : StarRing (ℤ√d)

Equations

• Zsqrtd.instStarRing = StarRing.mk ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[simp]

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

@[deprecated Zsqrtd.natCast_re]

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

Alias of Zsqrtd.natCast_re.

@[deprecated Zsqrtd.natCast_im]

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

Alias of Zsqrtd.natCast_im.

@[deprecated Zsqrtd.natCast_val]

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

Alias of Zsqrtd.natCast_val.

@[deprecated Zsqrtd.intCast_re]

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

Alias of Zsqrtd.intCast_re.

@[deprecated Zsqrtd.intCast_im]

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

Alias of Zsqrtd.intCast_im.

@[deprecated Zsqrtd.intCast_val]

theorem Zsqrtd.coe_int_val {d : ℤ} (n : ℤ) : ↑n = { re := n, im := 0 }

Alias of Zsqrtd.intCast_val.

@[deprecated Zsqrtd.ofInt_eq_intCast]

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

Alias of Zsqrtd.ofInt_eq_intCast.

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

@[deprecated Int.cast_add]

theorem Zsqrtd.coe_int_add {R : Type u} [AddGroupWithOne R] (m n : ℤ) : ↑(m + n) = ↑m + ↑n

Alias of Int.cast_add.

@[deprecated Int.cast_sub]

theorem Zsqrtd.coe_int_sub {R : Type u} [AddGroupWithOne R] (m n : ℤ) : ↑(m - n) = ↑m - ↑n

Alias of Int.cast_sub.

@[deprecated Int.cast_mul]

theorem Zsqrtd.coe_int_mul {α : Type u_1} [NonAssocRing α] (m n : ℤ) : ↑(m * n) = ↑m * ↑n

Alias of Int.cast_mul.

@[deprecated Int.cast_inj]

theorem Zsqrtd.coe_int_inj {α : Type u_3} [AddGroupWithOne α] [CharZero α] {m n : ℤ} : ↑m = ↑n ↔ m = n

Alias of Int.cast_inj.

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

@[deprecated Zsqrtd.intCast_dvd]

theorem Zsqrtd.coe_int_dvd_iff {d : ℤ} (z : ℤ) (a : ℤ√d) : ↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im

Alias of Zsqrtd.intCast_dvd.

@[deprecated Zsqrtd.intCast_dvd_intCast]

theorem Zsqrtd.coe_int_dvd_coe_int {d : ℤ} (a b : ℤ) : ↑a ∣ ↑b ↔ a ∣ b

Alias of Zsqrtd.intCast_dvd_intCast.

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

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

• Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.ofNat b) = True
• Zsqrtd.Nonnegg c d (Int.ofNat a) (Int.negSucc b) = Zsqrtd.SqLe (b + 1) c a d
• Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.ofNat b) = Zsqrtd.SqLe (a + 1) d b c
• Zsqrtd.Nonnegg c d (Int.negSucc a) (Int.negSucc a_1) = False

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

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

theorem Zsqrtd.norm_def {d : ℤ} (n : ℤ√d) : n.norm = 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_intCast {d : ℤ} (n : ℤ) : (↑n).norm = n * n

@[deprecated Zsqrtd.norm_intCast]

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

Alias of Zsqrtd.norm_intCast.

@[simp]

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

@[deprecated Zsqrtd.norm_natCast]

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

Alias of Zsqrtd.norm_natCast.

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

Equations

• Zsqrtd.normMonoidHom = { toFun := Zsqrtd.norm, map_one' := ⋯, map_mul' := ⋯ }

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 : ℤ} {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.

Equations

• { re := a, im := b }.Nonneg = Zsqrtd.Nonnegg d 1 a b

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

Equations

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

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

Equations

• Zsqrtd.instLTCastInt = { 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 a.Nonneg

Equations

• { re := a, im := b }.decidableNonneg = Zsqrtd.decidableNonnegg d 1 a b

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

Equations

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

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)

Equations

• Zsqrtd.preorder = Preorder.mk ⋯ ⋯ ⋯

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) : (Zsqrtd.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) : ¬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} : 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

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

Equations

• Zsqrtd.linearOrder = LinearOrder.mk ⋯ Zsqrtd.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE ⋯ ⋯ ⋯

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

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

Equations

• Zsqrtd.instLinearOrderedCommRingCastInt = LinearOrderedCommRing.mk ⋯

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

Equations

• Zsqrtd.instLinearOrderedRingCastInt = inferInstance

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

Equations

• Zsqrtd.instOrderedRingCastInt = inferInstance

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 Zsqrtd.sqrtd = g Zsqrtd.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) : ↑(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

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

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