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

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
instance instDecidableEqZsqrtd :
{d : } →
Equations
• instDecidableEqZsqrtd = decEqZsqrtd✝
Equations
Instances For
def Zsqrtd.ofInt {d : } (n : ) :

Convert an integer to a ℤ√d

Equations
• = { re := n, im := 0 }
Instances For
theorem Zsqrtd.ofInt_re {d : } (n : ) :
().re = n
theorem Zsqrtd.ofInt_im {d : } (n : ) :
().im = 0
instance Zsqrtd.instZero {d : } :

The zero of the ring

Equations
• Zsqrtd.instZero = { zero := }
@[simp]
theorem Zsqrtd.zero_re {d : } :
= 0
@[simp]
theorem Zsqrtd.zero_im {d : } :
= 0
Equations
• Zsqrtd.instInhabited = { default := 0 }
instance Zsqrtd.instOne {d : } :

The one of the ring

Equations
• Zsqrtd.instOne = { one := }
@[simp]
theorem Zsqrtd.one_re {d : } :
= 1
@[simp]
theorem Zsqrtd.one_im {d : } :
= 0
def Zsqrtd.sqrtd {d : } :

The representative of √d in the ring

Equations
• Zsqrtd.sqrtd = { re := 0, im := 1 }
Instances For
@[simp]
theorem Zsqrtd.sqrtd_re {d : } :
Zsqrtd.sqrtd.re = 0
@[simp]
theorem Zsqrtd.sqrtd_im {d : } :
Zsqrtd.sqrtd.im = 1
instance Zsqrtd.instAdd {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 : ℤ√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
instance Zsqrtd.instNeg {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 : } :

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 : ℤ√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 : } :
Equations
@[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 : } :
Equations
instance Zsqrtd.commRing {d : } :
Equations
• Zsqrtd.commRing = let __src := Zsqrtd.addGroupWithOne;
Equations
instance Zsqrtd.instMonoid {d : } :
Equations
• Zsqrtd.instMonoid = inferInstance
Equations
• Zsqrtd.instCommMonoid = inferInstance
instance Zsqrtd.instCommSemigroup {d : } :
Equations
• Zsqrtd.instCommSemigroup = inferInstance
Equations
• Zsqrtd.instSemigroup = inferInstance
Equations
instance Zsqrtd.instAddSemigroup {d : } :
Equations
instance Zsqrtd.instCommSemiring {d : } :
Equations
• Zsqrtd.instCommSemiring = inferInstance
Equations
• Zsqrtd.instSemiring = inferInstance
instance Zsqrtd.instRing {d : } :
Equations
• Zsqrtd.instRing = inferInstance
Equations
• Zsqrtd.instDistrib = inferInstance
instance Zsqrtd.instStar {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
Equations
• Zsqrtd.instStarRing =
Equations
• =
@[simp]
theorem Zsqrtd.natCast_re {d : } (n : ) :
(n).re = n
@[simp]
theorem Zsqrtd.ofNat_re {d : } (n : ) [n.AtLeastTwo] :
().re = n
@[simp]
theorem Zsqrtd.natCast_im {d : } (n : ) :
(n).im = 0
@[simp]
theorem Zsqrtd.ofNat_im {d : } (n : ) [n.AtLeastTwo] :
().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 }
Equations
• =
@[simp]
theorem Zsqrtd.ofInt_eq_intCast {d : } (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 : ) :
= 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
theorem Zsqrtd.coe_int_add {R : Type u} [] (m : ) (n : ) :
(m + n) = m + n

Alias of Int.cast_add.

@[deprecated Int.cast_sub]
theorem Zsqrtd.coe_int_sub {R : Type u} [] (m : ) (n : ) :
(m - n) = m - n

Alias of Int.cast_sub.

@[deprecated Int.cast_mul]
theorem Zsqrtd.coe_int_mul {α : Type u_1} [] (m : ) (n : ) :
(m * n) = m * n

Alias of Int.cast_mul.

@[deprecated Int.cast_inj]
theorem Zsqrtd.coe_int_inj {α : Type u_3} [] [] {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 : ℤ√d} {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 : ℤ√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 < 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
Instances For
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 dZsqrtd.SqLe z 1 w dZsqrtd.SqLe (x * w + y * z) d (x * z + d * y * w) 1) (Zsqrtd.SqLe x 1 y dZsqrtd.SqLe w d z 1Zsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (Zsqrtd.SqLe y d x 1Zsqrtd.SqLe z 1 w dZsqrtd.SqLe (x * z + d * y * w) 1 (x * w + y * z) d) (Zsqrtd.SqLe y d x 1Zsqrtd.SqLe w d z 1Zsqrtd.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.
Instances For
theorem Zsqrtd.nonnegg_comm {c : } {d : } {x : } {y : } :
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 = -xZsqrtd.SqLe x c a d)Zsqrtd.Nonnegg c d (a) b
theorem Zsqrtd.nonnegg_cases_left {c : } {d : } {b : } {a : } (h : ∀ (x : ), a = -xZsqrtd.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
Instances For
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
@[simp]
theorem Zsqrtd.norm_one {d : } :
= 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 : ℤ√d) (m : ℤ√d) :
(n * m).norm = n.norm * m.norm

norm as a MonoidHom.

Equations
• Zsqrtd.normMonoidHom = { toFun := Zsqrtd.norm, map_one' := , map_mul' := }
Instances For
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
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 : ℤ√d} {y : ℤ√d} (h : ) :
x.norm = y.norm
def Zsqrtd.Nonneg {d : } :
ℤ√dProp

Nonnegativity of an element of ℤ√d.

Equations
Instances For
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 : ) :
Equations
• One or more equations did not get rendered due to their size.
instance Zsqrtd.decidableNonneg {d : } (a : ℤ√d) :
Decidable a.Nonneg
Equations
instance Zsqrtd.decidableLE {d : } :
DecidableRel fun (x x_1 : ℤ√d) => x x_1
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 : ℤ√d} {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 : ℤ√d) (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 : ℤ√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 : 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 : ℤ√d} {b : ℤ√d} (ha : a.Nonneg) (hb : b.Nonneg) :
(a * b).Nonneg
theorem Zsqrtd.mul_nonneg {d : } (a : ℤ√d) (b : ℤ√d) :
0 a0 b0 a * b
theorem Zsqrtd.not_sqLe_succ (c : ) (d : ) (y : ) (h : 0 < c) :
¬Zsqrtd.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 : } [self : ] (n : ) :
x n * n
theorem Zsqrtd.Nonsquare.ns (x : ) [] (n : ) :
x n * n
theorem Zsqrtd.d_pos {d : } [dnsq : ] :
0 < d
theorem Zsqrtd.divides_sq_eq_zero {d : } [dnsq : ] {x : } {y : } (h : x * x = d * y * y) :
x = 0 y = 0
theorem Zsqrtd.divides_sq_eq_zero_z {d : } [dnsq : ] {x : } {y : } (h : x * x = d * y * y) :
x = 0 y = 0
theorem Zsqrtd.not_divides_sq {d : } [dnsq : ] (x : ) (y : ) :
(x + 1) * (x + 1) d * (y + 1) * (y + 1)
theorem Zsqrtd.nonneg_antisymm {d : } [dnsq : ] {a : ℤ√d} :
a.Nonneg(-a).Nonnega = 0
theorem Zsqrtd.le_antisymm {d : } [dnsq : ] {a : ℤ√d} {b : ℤ√d} (ab : a b) (ba : b a) :
a = b
instance Zsqrtd.linearOrder {d : } [dnsq : ] :
Equations
• Zsqrtd.linearOrder = let __src := Zsqrtd.preorder; LinearOrder.mk Zsqrtd.decidableLE decidableEqOfDecidableLE decidableLTOfDecidableLE
theorem Zsqrtd.eq_zero_or_eq_zero_of_mul_eq_zero {d : } [dnsq : ] {a : ℤ√d} {b : ℤ√d} :
a * b = 0a = 0 b = 0
Equations
• =
instance Zsqrtd.instIsDomainCastInt {d : } [dnsq : ] :
Equations
• =
theorem Zsqrtd.mul_pos {d : } [dnsq : ] (a : ℤ√d) (b : ℤ√d) (a0 : 0 < a) (b0 : 0 < b) :
0 < a * b
instance Zsqrtd.instLinearOrderedCommRingCastInt {d : } [dnsq : ] :
Equations
• Zsqrtd.instLinearOrderedCommRingCastInt = let __src := Zsqrtd.commRing; let __src_1 := Zsqrtd.linearOrder; let __src_2 := ;
instance Zsqrtd.instLinearOrderedRingCastInt {d : } [dnsq : ] :
Equations
• Zsqrtd.instLinearOrderedRingCastInt = inferInstance
instance Zsqrtd.instOrderedRingCastInt {d : } [dnsq : ] :
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 : ℤ√d →+* R) (g : ℤ√d →+* R) (h : f Zsqrtd.sqrtd = g Zsqrtd.sqrtd) :
f = g
@[simp]
theorem Zsqrtd.lift_symm_apply_coe {R : Type} [] {d : } (f : ℤ√d →+* R) :
(Zsqrtd.lift.symm f) = f Zsqrtd.sqrtd
@[simp]
theorem Zsqrtd.lift_apply_apply {R : Type} [] {d : } (r : { r : R // r * r = d }) (a : ℤ√d) :
(Zsqrtd.lift r) a = a.re + a.im * r
def Zsqrtd.lift {R : Type} [] {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.
Instances For
theorem Zsqrtd.lift_injective {R : Type} [] [] {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.