mathlib documentation

data.zsqrtd.basic

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

source
@[protected, instance]
def zsqrtd.decidable_eq {d : ℤ} :
decidable_eq (ℤ√d)
Equations
source
theorem zsqrtd.ext {d : ℤ} {z w : ℤ√d} :
z = w ↔ z.re = w.re ∧ z.im = w.im
source
def zsqrtd.of_int {d : ℤ} (n : ℤ) :
ℤ√d

Convert an integer to a ℤ√d

Equations
source
theorem zsqrtd.of_int_re {d : ℤ} (n : ℤ) :
(zsqrtd.of_int n).re = n
source
theorem zsqrtd.of_int_im {d : ℤ} (n : ℤ) :
(zsqrtd.of_int n).im = 0
source
def zsqrtd.zero {d : ℤ} :
ℤ√d

The zero of the ring

Equations
source
@[protected, instance]
def zsqrtd.has_zero {d : ℤ} :
has_zero (ℤ√d)
Equations
source
@[simp]
theorem zsqrtd.zero_re {d : ℤ} :
0.re = 0
source
@[simp]
theorem zsqrtd.zero_im {d : ℤ} :
0.im = 0
source
@[protected, instance]
def zsqrtd.inhabited {d : ℤ} :
inhabited (ℤ√d)
Equations
source
def zsqrtd.one {d : ℤ} :
ℤ√d

The one of the ring

Equations
source
@[protected, instance]
def zsqrtd.has_one {d : ℤ} :
has_one (ℤ√d)
Equations
source
@[simp]
theorem zsqrtd.one_re {d : ℤ} :
1.re = 1
source
@[simp]
theorem zsqrtd.one_im {d : ℤ} :
1.im = 0
source
def zsqrtd.sqrtd {d : ℤ} :
ℤ√d

The representative of √d in the ring

Equations
source
@[simp]
theorem zsqrtd.sqrtd_re {d : ℤ} :
zsqrtd.sqrtd.re = 0
source
@[simp]
theorem zsqrtd.sqrtd_im {d : ℤ} :
zsqrtd.sqrtd.im = 1
source
def zsqrtd.add {d : ℤ} :
ℤ√d → ℤ√d → ℤ√d

Addition of elements of ℤ√d

Equations
source
@[protected, instance]
def zsqrtd.has_add {d : ℤ} :
has_add (ℤ√d)
Equations
source
@[simp]
theorem zsqrtd.add_def {d : ℤ} (x y x' y' : ℤ) :
{re := x, im := y} + {re := x', im := y'} = {re := x + x', im := y + y'}
source
@[simp]
theorem zsqrtd.add_re {d : ℤ} (z w : ℤ√d) :
(z + w).re = z.re + w.re
source
@[simp]
theorem zsqrtd.add_im {d : ℤ} (z w : ℤ√d) :
(z + w).im = z.im + w.im
source
@[simp]
theorem zsqrtd.bit0_re {d : ℤ} (z : ℤ√d) :
(bit0 z).re = bit0 z.re
source
@[simp]
theorem zsqrtd.bit0_im {d : ℤ} (z : ℤ√d) :
(bit0 z).im = bit0 z.im
source
@[simp]
theorem zsqrtd.bit1_re {d : ℤ} (z : ℤ√d) :
(bit1 z).re = bit1 z.re
source
@[simp]
theorem zsqrtd.bit1_im {d : ℤ} (z : ℤ√d) :
(bit1 z).im = bit0 z.im
source
def zsqrtd.neg {d : ℤ} :
ℤ√d → ℤ√d

Negation in ℤ√d

Equations
source
@[protected, instance]
def zsqrtd.has_neg {d : ℤ} :
has_neg (ℤ√d)
Equations
source
@[simp]
theorem zsqrtd.neg_re {d : ℤ} (z : ℤ√d) :
(-z).re = -z.re
source
@[simp]
theorem zsqrtd.neg_im {d : ℤ} (z : ℤ√d) :
(-z).im = -z.im
source
def zsqrtd.mul {d : ℤ} :
ℤ√d → ℤ√d → ℤ√d

Multiplication in ℤ√d

Equations
source
@[protected, instance]
def zsqrtd.has_mul {d : ℤ} :
has_mul (ℤ√d)
Equations
source
@[simp]
theorem zsqrtd.mul_re {d : ℤ} (z w : ℤ√d) :
(z * w).re = (z.re) * w.re + (d * z.im) * w.im
source
@[simp]
theorem zsqrtd.mul_im {d : ℤ} (z w : ℤ√d) :
(z * w).im = (z.re) * w.im + (z.im) * w.re
source
@[protected, instance]
def zsqrtd.comm_ring {d : ℤ} :
comm_ring (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.add_comm_monoid {d : ℤ} :
add_comm_monoid (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.add_monoid {d : ℤ} :
add_monoid (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.monoid {d : ℤ} :
monoid (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.comm_monoid {d : ℤ} :
comm_monoid (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.comm_semigroup {d : ℤ} :
comm_semigroup (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.semigroup {d : ℤ} :
semigroup (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.add_comm_semigroup {d : ℤ} :
add_comm_semigroup (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.add_semigroup {d : ℤ} :
add_semigroup (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.comm_semiring {d : ℤ} :
comm_semiring (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.semiring {d : ℤ} :
semiring (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.ring {d : ℤ} :
ring (ℤ√d)
Equations
source
@[protected, instance]
def zsqrtd.distrib {d : ℤ} :
distrib (ℤ√d)
Equations
source
def zsqrtd.conj {d : ℤ} :
ℤ√d → ℤ√d

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

Equations
source
@[simp]
theorem zsqrtd.conj_re {d : ℤ} (z : ℤ√d) :
z.conj.re = z.re
source
@[simp]
theorem zsqrtd.conj_im {d : ℤ} (z : ℤ√d) :
z.conj.im = -z.im
source
def zsqrtd.conj_hom {d : ℤ} :
ℤ√d →+ ℤ√d

conj as an add_monoid_hom.

Equations
source
@[simp]
theorem zsqrtd.conj_zero {d : ℤ} :
0.conj = 0
source
@[simp]
theorem zsqrtd.conj_one {d : ℤ} :
1.conj = 1
source
@[simp]
theorem zsqrtd.conj_neg {d : ℤ} (x : ℤ√d) :
(-x).conj = -x.conj
source
@[simp]
theorem zsqrtd.conj_add {d : ℤ} (x y : ℤ√d) :
(x + y).conj = x.conj + y.conj
source
@[simp]
theorem zsqrtd.conj_sub {d : ℤ} (x y : ℤ√d) :
(x - y).conj = x.conj - y.conj
source
@[simp]
theorem zsqrtd.conj_conj {d : ℤ} (x : ℤ√d) :
x.conj.conj = x
source
@[protected, instance]
def zsqrtd.nontrivial {d : ℤ} :
nontrivial (ℤ√d)
source
@[simp]
theorem zsqrtd.coe_nat_re {d : ℤ} (n : ℕ) :
↑n.re = ↑n
source
@[simp]
theorem zsqrtd.coe_nat_im {d : ℤ} (n : ℕ) :
↑n.im = 0
source
theorem zsqrtd.coe_nat_val {d : ℤ} (n : ℕ) :
↑n = {re := ↑n, im := 0}
source
@[simp]
theorem zsqrtd.coe_int_re {d : ℤ} (n : ℤ) :
↑n.re = n
source
@[simp]
theorem zsqrtd.coe_int_im {d : ℤ} (n : ℤ) :
↑n.im = 0
source
theorem zsqrtd.coe_int_val {d : ℤ} (n : ℤ) :
↑n = {re := n, im := 0}
source
@[protected, instance]
def zsqrtd.char_zero {d : ℤ} :
char_zero (ℤ√d)
source
@[simp]
theorem zsqrtd.of_int_eq_coe {d : ℤ} (n : ℤ) :
zsqrtd.of_int n = ↑n
source
@[simp]
theorem zsqrtd.smul_val {d : ℤ} (n x y : ℤ) :
(↑n) * {re := x, im := y} = {re := n * x, im := n * y}
source
@[simp]
theorem zsqrtd.muld_val {d : ℤ} (x y : ℤ) :
zsqrtd.sqrtd * {re := x, im := y} = {re := d * y, im := x}
source
@[simp]
theorem zsqrtd.dmuld {d : ℤ} :
zsqrtd.sqrtd * zsqrtd.sqrtd = ↑d
source
@[simp]
theorem zsqrtd.smuld_val {d : ℤ} (n x y : ℤ) :
(zsqrtd.sqrtd * ↑n) * {re := x, im := y} = {re := (d * n) * y, im := n * x}
source
theorem zsqrtd.decompose {d x y : ℤ} :
{re := x, im := y} = ↑x + zsqrtd.sqrtd * ↑y
source
theorem zsqrtd.mul_conj {d x y : ℤ} :
{re := x, im := y} * {re := x, im := y}.conj = (↑x) * ↑x - ((↑d) * ↑y) * ↑y
source
theorem zsqrtd.conj_mul {d : ℤ} {a b : ℤ√d} :
(a * b).conj = (a.conj) * b.conj
source
@[protected]
theorem zsqrtd.coe_int_add {d : ℤ} (m n : ℤ) :
↑(m + n) = ↑m + ↑n
source
@[protected]
theorem zsqrtd.coe_int_sub {d : ℤ} (m n : ℤ) :
↑(m - n) = ↑m - ↑n
source
@[protected]
theorem zsqrtd.coe_int_mul {d : ℤ} (m n : ℤ) :
↑m * n = (↑m) * ↑n
source
@[protected]
theorem zsqrtd.coe_int_inj {d m n : ℤ} (h : ↑m = ↑n) :
m = n
source
theorem zsqrtd.coe_int_dvd_iff {d : ℤ} (z : ℤ) (a : ℤ√d) :
↑z ∣ a ↔ z ∣ a.re ∧ z ∣ a.im
source
def zsqrtd.sq_le (a c b d : ℕ) :
Prop

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

Equations
source
theorem zsqrtd.sq_le_of_le {c d x y z w : ℕ} (xz : z ≤ x) (yw : y ≤ w) (xy : zsqrtd.sq_le x c y d) :
zsqrtd.sq_le z c w d
source
theorem zsqrtd.sq_le_add_mixed {c d x y z w : ℕ} (xy : zsqrtd.sq_le x c y d) (zw : zsqrtd.sq_le z c w d) :
c * x * z ≤ d * y * w
source
theorem zsqrtd.sq_le_add {c d x y z w : ℕ} (xy : zsqrtd.sq_le x c y d) (zw : zsqrtd.sq_le z c w d) :
zsqrtd.sq_le (x + z) c (y + w) d
source
theorem zsqrtd.sq_le_cancel {c d x y z w : ℕ} (zw : zsqrtd.sq_le y d x c) (h : zsqrtd.sq_le (x + z) c (y + w) d) :
zsqrtd.sq_le z c w d
source
theorem zsqrtd.sq_le_smul {c d x y : ℕ} (n : ℕ) (xy : zsqrtd.sq_le x c y d) :
zsqrtd.sq_le (n * x) c (n * y) d
source
theorem zsqrtd.sq_le_mul {d x y z w : ℕ} :
(zsqrtd.sq_le x 1 y d → zsqrtd.sq_le z 1 w d → zsqrtd.sq_le (x * w + y * z) d (x * z + (d * y) * w) 1) ∧ (zsqrtd.sq_le x 1 y d → zsqrtd.sq_le w d z 1 → zsqrtd.sq_le (x * z + (d * y) * w) 1 (x * w + y * z) d) ∧ (zsqrtd.sq_le y d x 1 → zsqrtd.sq_le z 1 w d → zsqrtd.sq_le (x * z + (d * y) * w) 1 (x * w + y * z) d) ∧ (zsqrtd.sq_le y d x 1 → zsqrtd.sq_le w d z 1 → zsqrtd.sq_le (x * w + y * z) d (x * z + (d * y) * w) 1)
source
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
source
theorem zsqrtd.nonnegg_comm {c d : ℕ} {x y : ℤ} :
zsqrtd.nonnegg c d x y = zsqrtd.nonnegg d c y x
source
theorem zsqrtd.nonnegg_neg_pos {c d a b : ℕ} :
zsqrtd.nonnegg c d (-↑a) ↑b ↔ zsqrtd.sq_le a d b c
source
theorem zsqrtd.nonnegg_pos_neg {c d a b : ℕ} :
zsqrtd.nonnegg c d ↑a (-↑b) ↔ zsqrtd.sq_le b c a d
source
theorem zsqrtd.nonnegg_cases_right {c d a : ℕ} {b : ℤ} :
(∀ (x : ℕ), b = -↑x → zsqrtd.sq_le x c a d) → zsqrtd.nonnegg c d ↑a b
source
theorem zsqrtd.nonnegg_cases_left {c d b : ℕ} {a : ℤ} (h : ∀ (x : ℕ), a = -↑x → zsqrtd.sq_le x d b c) :
zsqrtd.nonnegg c d a ↑b
source
def zsqrtd.norm {d : ℤ} (n : ℤ√d) :
ℤ
Equations
source
theorem zsqrtd.norm_def {d : ℤ} (n : ℤ√d) :
n.norm = (n.re) * n.re - (d * n.im) * n.im
source
@[simp]
theorem zsqrtd.norm_zero {d : ℤ} :
0.norm = 0
source
@[simp]
theorem zsqrtd.norm_one {d : ℤ} :
1.norm = 1
source
@[simp]
theorem zsqrtd.norm_int_cast {d : ℤ} (n : ℤ) :
↑n.norm = n * n
source
@[simp]
theorem zsqrtd.norm_nat_cast {d : ℤ} (n : ℕ) :
↑n.norm = (↑n) * ↑n
source
@[simp]
theorem zsqrtd.norm_mul {d : ℤ} (n m : ℤ√d) :
(n * m).norm = (n.norm) * m.norm
source
def zsqrtd.norm_monoid_hom {d : ℤ} :
ℤ√d →* ℤ

norm as a monoid_hom.

Equations
source
theorem zsqrtd.norm_eq_mul_conj {d : ℤ} (n : ℤ√d) :
↑(n.norm) = n * n.conj
source
@[simp]
theorem zsqrtd.norm_neg {d : ℤ} (x : ℤ√d) :
(-x).norm = x.norm
source
@[simp]
theorem zsqrtd.norm_conj {d : ℤ} (x : ℤ√d) :
x.conj.norm = x.norm
source
@[protected, instance]
def zsqrtd.norm.is_monoid_hom {d : ℤ} :
is_monoid_hom zsqrtd.norm
source
theorem zsqrtd.norm_nonneg {d : ℤ} (hd : d ≤ 0) (n : ℤ√d) :
0 ≤ n.norm
source
theorem zsqrtd.norm_eq_one_iff {d : ℤ} {x : ℤ√d} :
x.norm.nat_abs = 1 ↔ is_unit x
source
theorem zsqrtd.is_unit_iff_norm_is_unit {d : ℤ} (z : ℤ√d) :
is_unit z ↔ is_unit z.norm
source
theorem zsqrtd.norm_eq_one_iff' {d : ℤ} (hd : d ≤ 0) (z : ℤ√d) :
z.norm = 1 ↔ is_unit z
source
theorem zsqrtd.norm_eq_zero_iff {d : ℤ} (hd : d < 0) (z : ℤ√d) :
z.norm = 0 ↔ z = 0
source
theorem zsqrtd.norm_eq_of_associated {d : ℤ} (hd : d ≤ 0) {x y : ℤ√d} (h : associated x y) :
x.norm = y.norm
source
def zsqrtd.nonneg {d : ℕ} :
ℤ√↑d → Prop

Nonnegativity of an element of ℤ√d.

Equations
source
@[protected]
def zsqrtd.le {d : ℕ} (a b : ℤ√↑d) :
Prop
Equations
source
@[protected, instance]
def zsqrtd.has_le {d : ℕ} :
has_le (ℤ√↑d)
Equations
source
@[protected]
def zsqrtd.lt {d : ℕ} (a b : ℤ√↑d) :
Prop
Equations
source
@[protected, instance]
def zsqrtd.has_lt {d : ℕ} :
has_lt (ℤ√↑d)
Equations
source
@[protected, instance]
def zsqrtd.decidable_nonnegg (c d : ℕ) (a b : ℤ) :
decidable (zsqrtd.nonnegg c d a b)
Equations
source
@[protected, instance]
def zsqrtd.decidable_nonneg {d : ℕ} (a : ℤ√↑d) :
decidable a.nonneg
Equations
source
@[protected, instance]
def zsqrtd.decidable_le {d : ℕ} (a b : ℤ√↑d) :
decidable (a ≤ b)
Equations
source
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})
source
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
source
theorem zsqrtd.nonneg_add {d : ℕ} {a b : ℤ√↑d} (ha : a.nonneg) (hb : b.nonneg) :
(a + b).nonneg
source
theorem zsqrtd.le_refl {d : ℕ} (a : ℤ√↑d) :
a ≤ a
source
@[protected]
theorem zsqrtd.le_trans {d : ℕ} {a b c : ℤ√↑d} (ab : a ≤ b) (bc : b ≤ c) :
a ≤ c
source
theorem zsqrtd.nonneg_iff_zero_le {d : ℕ} {a : ℤ√↑d} :
a.nonneg ↔ 0 ≤ a
source
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}
source
theorem zsqrtd.le_arch {d : ℕ} (a : ℤ√↑d) :
∃ (n : ℕ), a ≤ ↑n
source
@[protected]
theorem zsqrtd.nonneg_total {d : ℕ} (a : ℤ√↑d) :
a.nonneg ∨ (-a).nonneg
source
@[protected]
theorem zsqrtd.le_total {d : ℕ} (a b : ℤ√↑d) :
a ≤ b ∨ b ≤ a
source
@[protected, instance]
def zsqrtd.preorder {d : ℕ} :
preorder (ℤ√↑d)
Equations
source
@[protected]
theorem zsqrtd.add_le_add_left {d : ℕ} (a b : ℤ√↑d) (ab : a ≤ b) (c : ℤ√↑d) :
c + a ≤ c + b
source
@[protected]
theorem zsqrtd.le_of_add_le_add_left {d : ℕ} (a b c : ℤ√↑d) (h : c + a ≤ c + b) :
a ≤ b
source
@[protected]
theorem zsqrtd.add_lt_add_left {d : ℕ} (a b : ℤ√↑d) (h : a < b) (c : ℤ√↑d) :
c + a < c + b
source
theorem zsqrtd.nonneg_smul {d : ℕ} {a : ℤ√↑d} {n : ℕ} (ha : a.nonneg) :
((↑n) * a).nonneg
source
theorem zsqrtd.nonneg_muld {d : ℕ} {a : ℤ√↑d} (ha : a.nonneg) :
(zsqrtd.sqrtd * a).nonneg
source
theorem zsqrtd.nonneg_mul_lem {d x y : ℕ} {a : ℤ√↑d} (ha : a.nonneg) :
({re := ↑x, im := ↑y} * a).nonneg
source
theorem zsqrtd.nonneg_mul {d : ℕ} {a b : ℤ√↑d} (ha : a.nonneg) (hb : b.nonneg) :
(a * b).nonneg
source
@[protected]
theorem zsqrtd.mul_nonneg {d : ℕ} (a b : ℤ√↑d) :
0 ≤ a → 0 ≤ b → 0 ≤ a * b
source
theorem zsqrtd.not_sq_le_succ (c d y : ℕ) (h : 0 < c) :
¬zsqrtd.sq_le (y + 1) c 0 d
source
@[class]
structure 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.

Instances
source
theorem zsqrtd.d_pos {d : ℕ} [dnsq : zsqrtd.nonsquare d] :
0 < d
source
theorem zsqrtd.divides_sq_eq_zero {d : ℕ} [dnsq : zsqrtd.nonsquare d] {x y : ℕ} (h : x * x = (d * y) * y) :
x = 0 ∧ y = 0
source
theorem zsqrtd.divides_sq_eq_zero_z {d : ℕ} [dnsq : zsqrtd.nonsquare d] {x y : ℤ} (h : x * x = ((↑d) * y) * y) :
x = 0 ∧ y = 0
source
theorem zsqrtd.not_divides_sq {d : ℕ} [dnsq : zsqrtd.nonsquare d] (x y : ℕ) :
(x + 1) * (x + 1) ≠ (d * (y + 1)) * (y + 1)
source
theorem zsqrtd.nonneg_antisymm {d : ℕ} [dnsq : zsqrtd.nonsquare d] {a : ℤ√↑d} :
a.nonneg → (-a).nonneg → a = 0
source
theorem zsqrtd.le_antisymm {d : ℕ} [dnsq : zsqrtd.nonsquare d] {a b : ℤ√↑d} (ab : a ≤ b) (ba : b ≤ a) :
a = b
source
@[protected, instance]
def zsqrtd.linear_order {d : ℕ} [dnsq : zsqrtd.nonsquare d] :
linear_order (ℤ√↑d)
Equations
source
@[protected]
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
source
@[protected, instance]
def zsqrtd.integral_domain {d : ℕ} [dnsq : zsqrtd.nonsquare d] :
integral_domain (ℤ√↑d)
Equations
source
@[protected]
theorem zsqrtd.mul_pos {d : ℕ} [dnsq : zsqrtd.nonsquare d] (a b : ℤ√↑d) (a0 : 0 < a) (b0 : 0 < b) :
0 < a * b
source
@[protected, instance]
def zsqrtd.linear_ordered_comm_ring {d : ℕ} [dnsq : zsqrtd.nonsquare d] :
linear_ordered_comm_ring (ℤ√↑d)
Equations
source
@[protected, instance]
def zsqrtd.linear_ordered_semiring {d : ℕ} [dnsq : zsqrtd.nonsquare d] :
linear_ordered_semiring (ℤ√↑d)
Equations
source
@[protected, instance]
def zsqrtd.ordered_semiring {d : ℕ} [dnsq : zsqrtd.nonsquare d] :
ordered_semiring (ℤ√↑d)
Equations
source
theorem zsqrtd.norm_eq_zero {d : ℤ} (h_nonsquare : ∀ (n : ℤ), d ≠ n * n) (a : ℤ√d) :
a.norm = 0 ↔ a = 0
source
@[ext]
theorem zsqrtd.hom_ext {R : Type} [comm_ring R] {d : ℤ} (f g : ℤ√d →+* R) (h : ⇑f zsqrtd.sqrtd = ⇑g zsqrtd.sqrtd) :
f = g
source
@[simp]
theorem zsqrtd.lift_symm_apply_coe {R : Type} [comm_ring R] {d : ℤ} (f : ℤ√d →+* R) :
↑(⇑(zsqrtd.lift.symm) f) = ⇑f zsqrtd.sqrtd
source
@[simp]
theorem zsqrtd.lift_apply_apply {R : Type} [comm_ring R] {d : ℤ} (r : {r // r * r = ↑d}) (a : ℤ√d) :
⇑(⇑zsqrtd.lift r) a = ↑(a.re) + (↑(a.im)) * ↑r
source
def zsqrtd.lift {R : Type} [comm_ring R] {d : ℤ} :
{r // r * r = ↑d} ≃ (ℤ√d →+* R)

The unique ring_hom 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
source
theorem zsqrtd.lift_injective {R : Type} [comm_ring R] [char_zero R] {d : ℤ} (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).