number_theory.zsqrtd.basic

structure zsqrtd (d : ℤ) :

re : ℤ
im : ℤ

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 zsqrtd

source

@[protected, instance]

def zsqrtd.decidable_eq {d : ℤ} :

decidable_eq (ℤ√d)

Equations

zsqrtd.decidable_eq = id (λ (_v : ℤ√d), _v.cases_on (λ (re im : ℤ) (w : ℤ√d), w.cases_on (λ (w_re w_im : ℤ), decidable.by_cases (λ (ᾰ : re = w_re), eq.rec (decidable.by_cases (λ (ᾰ : im = w_im), eq.rec (decidable.is_true _) ᾰ) (λ (ᾰ : ¬im = w_im), decidable.is_false _)) ᾰ) (λ (ᾰ : ¬re = w_re), decidable.is_false _))))

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

zsqrtd.of_int n = {re := n, im := 0}

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

@[protected, instance]

def zsqrtd.has_zero {d : ℤ} :

has_zero (ℤ√d)

The zero of the ring

Equations

zsqrtd.has_zero = {zero := zsqrtd.of_int 0}

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

zsqrtd.inhabited = {default := 0}

source

@[protected, instance]

def zsqrtd.has_one {d : ℤ} :

has_one (ℤ√d)

The one of the ring

Equations

zsqrtd.has_one = {one := zsqrtd.of_int 1}

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

zsqrtd.sqrtd = {re := 0, im := 1}

source

@[simp]

theorem zsqrtd.sqrtd_re {d : ℤ} :

zsqrtd.sqrtd.re = 0

source

@[simp]

theorem zsqrtd.sqrtd_im {d : ℤ} :

zsqrtd.sqrtd.im = 1

source

@[protected, instance]

def zsqrtd.has_add {d : ℤ} :

has_add (ℤ√d)

Addition of elements of ℤ√d

Equations

zsqrtd.has_add = {add := λ (z w : ℤ√d), {re := z.re + w.re, im := z.im + w.im}}

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

@[protected, instance]

def zsqrtd.has_neg {d : ℤ} :

has_neg (ℤ√d)

Negation in ℤ√d

Equations

zsqrtd.has_neg = {neg := λ (z : ℤ√d), {re := -z.re, im := -z.im}}

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

@[protected, instance]

def zsqrtd.has_mul {d : ℤ} :

has_mul (ℤ√d)

Multiplication in ℤ√d

Equations

zsqrtd.has_mul = {mul := λ (z w : ℤ√d), {re := z.re * w.re + d * z.im * w.im, im := z.re * w.im + z.im * w.re}}

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

add_comm_group (ℤ√d)

Equations

zsqrtd.add_comm_group = {add := has_add.add zsqrtd.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add zsqrtd.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg zsqrtd.has_neg, sub := λ (a b : ℤ√d), a + -b, sub_eq_add_neg := _, zsmul := zsmul_rec {neg := has_neg.neg zsqrtd.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}

source

@[protected, instance]

def zsqrtd.add_group_with_one {d : ℤ} :

add_group_with_one (ℤ√d)

Equations

zsqrtd.add_group_with_one = {int_cast := zsqrtd.of_int d, add := add_comm_group.add zsqrtd.add_comm_group, add_assoc := _, zero := add_comm_group.zero zsqrtd.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul zsqrtd.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg zsqrtd.add_comm_group, sub := add_comm_group.sub zsqrtd.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul zsqrtd.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), zsqrtd.of_int ↑n, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}

source

@[protected, instance]

def zsqrtd.comm_ring {d : ℤ} :

comm_ring (ℤ√d)

Equations

zsqrtd.comm_ring = {add := has_add.add zsqrtd.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul zsqrtd.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg zsqrtd.add_group_with_one, sub := add_group_with_one.sub zsqrtd.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul zsqrtd.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast zsqrtd.add_group_with_one, nat_cast := add_group_with_one.nat_cast zsqrtd.add_group_with_one, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul zsqrtd.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul zsqrtd.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[protected, instance]

def zsqrtd.add_monoid {d : ℤ} :

add_monoid (ℤ√d)

Equations

zsqrtd.add_monoid = add_monoid_with_one.to_add_monoid (ℤ√d)

source

@[protected, instance]

def zsqrtd.monoid {d : ℤ} :

monoid (ℤ√d)

Equations

zsqrtd.monoid = ring.to_monoid (ℤ√d)

source

@[protected, instance]

def zsqrtd.comm_monoid {d : ℤ} :

comm_monoid (ℤ√d)

Equations

zsqrtd.comm_monoid = comm_ring.to_comm_monoid (ℤ√d)

source

@[protected, instance]

def zsqrtd.comm_semigroup {d : ℤ} :

comm_semigroup (ℤ√d)

Equations

zsqrtd.comm_semigroup = non_unital_comm_ring.to_comm_semigroup (ℤ√d)

source

@[protected, instance]

def zsqrtd.semigroup {d : ℤ} :

semigroup (ℤ√d)

Equations

zsqrtd.semigroup = semigroup_with_zero.to_semigroup (ℤ√d)

source

@[protected, instance]

def zsqrtd.add_comm_semigroup {d : ℤ} :

add_comm_semigroup (ℤ√d)

Equations

zsqrtd.add_comm_semigroup = add_comm_monoid.to_add_comm_semigroup (ℤ√d)

source

@[protected, instance]

def zsqrtd.add_semigroup {d : ℤ} :

add_semigroup (ℤ√d)

Equations

zsqrtd.add_semigroup = add_monoid.to_add_semigroup (ℤ√d)

source

@[protected, instance]

def zsqrtd.comm_semiring {d : ℤ} :

comm_semiring (ℤ√d)

Equations

zsqrtd.comm_semiring = comm_ring.to_comm_semiring

source

@[protected, instance]

def zsqrtd.semiring {d : ℤ} :

semiring (ℤ√d)

Equations

zsqrtd.semiring = ring.to_semiring

source

@[protected, instance]

def zsqrtd.ring {d : ℤ} :

ring (ℤ√d)

Equations

zsqrtd.ring = comm_ring.to_ring (ℤ√d)

source

@[protected, instance]

def zsqrtd.distrib {d : ℤ} :

distrib (ℤ√d)

Equations

zsqrtd.distrib = ring.to_distrib (ℤ√d)

source

@[protected, instance]

def zsqrtd.has_star {d : ℤ} :

has_star (ℤ√d)

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

Equations

zsqrtd.has_star = {star := λ (z : ℤ√d), {re := z.re, im := -z.im}}

source

@[simp]

theorem zsqrtd.star_mk {d : ℤ} (x y : ℤ) :

has_star.star {re := x, im := y} = {re := x, im := -y}

source

@[simp]

theorem zsqrtd.star_re {d : ℤ} (z : ℤ√d) :

(has_star.star z).re = z.re

source

@[simp]

theorem zsqrtd.star_im {d : ℤ} (z : ℤ√d) :

(has_star.star z).im = -z.im

source

@[protected, instance]

def zsqrtd.star_ring {d : ℤ} :

star_ring (ℤ√d)

Equations

zsqrtd.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := zsqrtd.has_star d, star_involutive := _}, star_mul := _}, star_add := _}

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

theorem zsqrtd.smul_re {d : ℤ} (a : ℤ) (b : ℤ√d) :

(↑a * b).re = a * b.re

source

theorem zsqrtd.smul_im {d : ℤ} (a : ℤ) (b : ℤ√d) :

(↑a * b).im = a * b.im

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_star {d x y : ℤ} :

{re := x, im := y} * has_star.star {re := x, im := y} = ↑x * ↑x - ↑d * ↑y * ↑y

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

@[simp, norm_cast]

theorem zsqrtd.coe_int_dvd_coe_int {d : ℤ} (a b : ℤ) :

↑a ∣ ↑b ↔ a ∣ b

source

@[protected]

theorem zsqrtd.eq_of_smul_eq_smul_left {d a : ℤ} {b c : ℤ√d} (ha : a ≠ 0) (h : ↑a * b = ↑a * c) :

b = c

source

theorem zsqrtd.gcd_eq_zero_iff {d : ℤ} (a : ℤ√d) :

a.re.gcd a.im = 0 ↔ a = 0

source

theorem zsqrtd.gcd_pos_iff {d : ℤ} (a : ℤ√d) :

0 < a.re.gcd a.im ↔ a ≠ 0

source

theorem zsqrtd.coprime_of_dvd_coprime {d : ℤ} {a b : ℤ√d} (hcoprime : is_coprime a.re a.im) (hdvd : b ∣ a) :

is_coprime b.re b.im

source

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 ∧ is_coprime b.re b.im

source

def zsqrtd.sq_le (a c b d : ℕ) :

Prop

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

Equations

zsqrtd.sq_le a c b d = (c * a * a ≤ d * b * b)

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

zsqrtd.nonnegg c d -[1+ a] -[1+ b] = false
zsqrtd.nonnegg c d -[1+ a] ↑b = zsqrtd.sq_le (a + 1) d b c
zsqrtd.nonnegg c d ↑a -[1+ b] = zsqrtd.sq_le (b + 1) c a d
zsqrtd.nonnegg c d ↑a ↑b = true

Instances for zsqrtd.nonnegg

zsqrtd.decidable_nonnegg

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

ℤ

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

Equations

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

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

zsqrtd.norm_monoid_hom = {to_fun := zsqrtd.norm d, map_one' := _, map_mul' := _}

source

theorem zsqrtd.norm_eq_mul_conj {d : ℤ} (n : ℤ√d) :

↑(n.norm) = n * has_star.star n

source

@[simp]

theorem zsqrtd.norm_neg {d : ℤ} (x : ℤ√d) :

(-x).norm = x.norm

source

@[simp]

theorem zsqrtd.norm_conj {d : ℤ} (x : ℤ√d) :

(has_star.star x).norm = x.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

{re := a, im := b}.nonneg = zsqrtd.nonnegg d 1 a b

Instances for zsqrtd.nonneg

zsqrtd.decidable_nonneg

source

@[protected, instance]

def zsqrtd.has_le {d : ℕ} :

has_le (ℤ√↑d)

Equations

zsqrtd.has_le = {le := λ (a b : ℤ√↑d), (b - a).nonneg}

source

@[protected, instance]

def zsqrtd.has_lt {d : ℕ} :

has_lt (ℤ√↑d)

Equations

zsqrtd.has_lt = {lt := λ (a b : ℤ√↑d), ¬b ≤ a}

source

@[protected, instance]

def zsqrtd.decidable_nonnegg (c d : ℕ) (a b : ℤ) :

decidable (zsqrtd.nonnegg c d a b)

Equations

zsqrtd.decidable_nonnegg c d a b = a.cases_on (λ (a : ℕ), b.cases_on (λ (b : ℕ), _.mpr (_.mpr (_.mpr decidable.true))) (λ (b : ℕ), _.mpr (_.mpr ((c * (b + 1) * (b + 1)).decidable_le (d * a * a))))) (λ (a : ℕ), b.cases_on (λ (b : ℕ), _.mpr (_.mpr ((d * (a + 1) * (a + 1)).decidable_le (c * b * b)))) (λ (b : ℕ), _.mpr decidable.false))

source

@[protected, instance]

def zsqrtd.decidable_nonneg {d : ℕ} (a : ℤ√↑d) :

decidable a.nonneg

Equations

{re := a, im := b}.decidable_nonneg = zsqrtd.decidable_nonnegg d 1 a b

source

@[protected, instance]

def zsqrtd.decidable_le {d : ℕ} :

decidable_rel has_le.le

Equations

zsqrtd.decidable_le = λ (_x _x_1 : ℤ√↑d), (_x_1 - _x).decidable_nonneg

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

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

zsqrtd.preorder = {le := has_le.le zsqrtd.has_le, lt := has_lt.lt zsqrtd.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _}

source

theorem zsqrtd.le_arch {d : ℕ} (a : ℤ√↑d) :

∃ (n : ℕ), a ≤ ↑n

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

ns : ∀ (n : ℕ), x ≠ n * n

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 of this typeclass

pell.dnsq

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

zsqrtd.linear_order = {le := preorder.le zsqrtd.preorder, lt := preorder.lt zsqrtd.preorder, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_total := _, decidable_le := zsqrtd.decidable_le d, decidable_eq := decidable_eq_of_decidable_le zsqrtd.decidable_le, decidable_lt := decidable_lt_of_decidable_le zsqrtd.decidable_le, max := max_default (λ (a b : ℤ√↑d), zsqrtd.decidable_le a b), max_def := _, min := min_default (λ (a b : ℤ√↑d), zsqrtd.decidable_le a b), min_def := _}

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.no_zero_divisors {d : ℕ} [dnsq : zsqrtd.nonsquare d] :

no_zero_divisors (ℤ√↑d)

source

@[protected, instance]

def zsqrtd.is_domain {d : ℕ} [dnsq : zsqrtd.nonsquare d] :

is_domain (ℤ√↑d)

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

zsqrtd.linear_ordered_comm_ring = {add := comm_ring.add zsqrtd.comm_ring, add_assoc := _, zero := comm_ring.zero zsqrtd.comm_ring, zero_add := _, add_zero := _, nsmul := comm_ring.nsmul zsqrtd.comm_ring, nsmul_zero' := _, nsmul_succ' := _, neg := comm_ring.neg zsqrtd.comm_ring, sub := comm_ring.sub zsqrtd.comm_ring, sub_eq_add_neg := _, zsmul := comm_ring.zsmul zsqrtd.comm_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := comm_ring.int_cast zsqrtd.comm_ring, nat_cast := comm_ring.nat_cast zsqrtd.comm_ring, one := comm_ring.one zsqrtd.comm_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := comm_ring.mul zsqrtd.comm_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := comm_ring.npow zsqrtd.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, le := linear_order.le zsqrtd.linear_order, lt := linear_order.lt zsqrtd.linear_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, exists_pair_ne := _, zero_le_one := _, mul_pos := _, le_total := _, decidable_le := linear_order.decidable_le zsqrtd.linear_order, decidable_eq := linear_order.decidable_eq zsqrtd.linear_order, decidable_lt := linear_order.decidable_lt zsqrtd.linear_order, max := linear_order.max zsqrtd.linear_order, max_def := _, min := linear_order.min zsqrtd.linear_order, min_def := _, mul_comm := _}

source

@[protected, instance]

def zsqrtd.linear_ordered_ring {d : ℕ} [dnsq : zsqrtd.nonsquare d] :

linear_ordered_ring (ℤ√↑d)

Equations

zsqrtd.linear_ordered_ring = linear_ordered_comm_ring.to_linear_ordered_ring (ℤ√↑d)

source

@[protected, instance]

def zsqrtd.ordered_ring {d : ℕ} [dnsq : zsqrtd.nonsquare d] :

ordered_ring (ℤ√↑d)

Equations

zsqrtd.ordered_ring = strict_ordered_ring.to_ordered_ring

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

zsqrtd.lift = {to_fun := λ (r : {r // r * r = ↑d}), {to_fun := λ (a : ℤ√d), ↑(a.re) + ↑(a.im) * ↑r, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, inv_fun := λ (f : ℤ√d →+* R), ⟨⇑f zsqrtd.sqrtd, _⟩, left_inv := _, right_inv := _}

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

source

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.

source

theorem zsqrtd.mker_norm_eq_unitary {d : ℤ} :

monoid_hom.mker zsqrtd.norm_monoid_hom = unitary (ℤ√d)

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

mathlib3 documentation

ℤ[√d] #