@[protected, instance]
Convert an integer to a ℤ√d
Equations
- zsqrtd.of_int n = {re := n, im := 0}
@[protected, instance]
Equations
- zsqrtd.has_zero = {zero := zsqrtd.zero d}
@[protected, instance]
Equations
- zsqrtd.inhabited = {default := 0}
@[protected, instance]
Equations
- zsqrtd.has_one = {one := zsqrtd.one d}
The representative of √d
in the ring
Equations
- zsqrtd.sqrtd = {re := 0, im := 1}
@[protected, instance]
Equations
- zsqrtd.has_add = {add := zsqrtd.add d}
@[protected, instance]
Equations
- zsqrtd.has_neg = {neg := zsqrtd.neg d}
@[protected, instance]
Equations
- zsqrtd.has_mul = {mul := zsqrtd.mul d}
@[protected, instance]
Equations
- zsqrtd.comm_ring = {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 := _, gsmul := gsmul_rec {neg := zsqrtd.neg d}, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul zsqrtd.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul zsqrtd.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
conj
as an add_monoid_hom
.
Equations
- zsqrtd.conj_hom = {to_fun := zsqrtd.conj d, map_zero' := _, map_add' := _}
Read sq_le a c b d
as a √c ≤ b √d
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
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) :
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
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
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
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)
"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
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
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
norm
as a monoid_hom
.
Equations
- zsqrtd.norm_monoid_hom = {to_fun := zsqrtd.norm d, map_one' := _, map_mul' := _}
@[protected, instance]
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))
@[protected, instance]
Equations
- {re := a, im := b}.decidable_nonneg = zsqrtd.decidable_nonnegg d 1 a b
@[protected, instance]
Equations
- a.decidable_le b = (b - a).decidable_nonneg
theorem
zsqrtd.le_antisymm
{d : ℕ}
[dnsq : zsqrtd.nonsquare d]
{a b : ℤ√↑d}
(ab : a ≤ b)
(ba : b ≤ a) :
a = b
@[protected, instance]
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}
@[protected, instance]
Equations
- zsqrtd.integral_domain = {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 := _, gsmul := comm_ring.gsmul zsqrtd.comm_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul zsqrtd.comm_ring, mul_assoc := _, one := comm_ring.one zsqrtd.comm_ring, one_mul := _, mul_one := _, npow := comm_ring.npow zsqrtd.comm_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
@[protected]
@[protected, instance]
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 := _, gsmul := comm_ring.gsmul zsqrtd.comm_ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := comm_ring.mul zsqrtd.comm_ring, mul_assoc := _, one := comm_ring.one zsqrtd.comm_ring, 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 := _, 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, exists_pair_ne := _, mul_comm := _}
@[protected, instance]
@[protected, instance]
@[ext]
theorem
zsqrtd.hom_ext
{R : Type}
[comm_ring R]
{d : ℤ}
(f g : ℤ√d →+* R)
(h : ⇑f zsqrtd.sqrtd = ⇑g zsqrtd.sqrtd) :
f = g
@[simp]
theorem
zsqrtd.lift_symm_apply_coe
{R : Type}
[comm_ring R]
{d : ℤ}
(f : ℤ√d →+* R) :
↑(⇑(zsqrtd.lift.symm) f) = ⇑f zsqrtd.sqrtd
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
.