instance QuadraticInteger.field {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] : Fact (∀ (r : ℚ), r ^ 2 ≠ ↑d + 0 * r)

@[simp]

theorem QuadraticInteger.re_ratCast {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] (q : ℚ) : (↑q).re = q

@[simp]

theorem QuadraticInteger.im_ratCast {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] (q : ℚ) : (↑q).im = 0

theorem QuadraticInteger.ratCast_eq_coe {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] (q : ℚ) : ↑q = ↑q

@[simp]

theorem QuadraticInteger.re_intCast_K {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] (n : ℤ) : (↑n).re = ↑n

@[simp]

theorem QuadraticInteger.im_intCast_K {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] (n : ℤ) : (↑n).im = 0

theorem QuadraticInteger.rational_iff {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} : ↑a + b • QuadraticAlgebra.omega ∈ Set.range ⇑(algebraMap ℚ (QuadraticAlgebra ℚ (↑d) 0)) ↔ b = 0

theorem QuadraticInteger.minpoly {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hb : b ≠ 0) : _root_.minpoly ℚ (↑a + b • QuadraticAlgebra.omega) = Polynomial.X ^ 2 - Polynomial.C (2 * a) * Polynomial.X + Polynomial.C (a ^ 2 - ↑d * b ^ 2)

theorem QuadraticInteger.adjoin_z_eq_top {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (h : b ≠ 0) : ℚ⟮↑a + b • QuadraticAlgebra.omega⟯ = ⊤

theorem QuadraticInteger.trace {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} : (Algebra.trace ℚ (QuadraticAlgebra ℚ (↑d) 0)) (↑a + b • QuadraticAlgebra.omega) = 2 * a

theorem QuadraticInteger.norm {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} : (Algebra.norm ℚ) (↑a + b • QuadraticAlgebra.omega) = a ^ 2 - ↑d * b ^ 2

theorem QuadraticInteger.trace_int {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) : ∃ (t : ℤ), ↑t = 2 * a

theorem QuadraticInteger.a_half_int {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) (ha : ¬∃ (A : ℤ), ↑A = a) : ∃ (A : ℤ), ↑A = a - 2⁻¹

theorem QuadraticInteger.norm_int {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) : ∃ (n : ℤ), ↑n = a ^ 2 - ↑d * b ^ 2

noncomputable def QuadraticInteger.n {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) : ℤ

Equations

• QuadraticInteger.n hz = ⋯.choose

theorem QuadraticInteger.n_spec {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) : ↑(n hz) = a ^ 2 - ↑d * b ^ 2

theorem QuadraticInteger.four_n {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) : 4 * ↑(n hz) = (2 * a) ^ 2 - ↑d * (2 * b) ^ 2

theorem QuadraticInteger.squarefree_mul {n : ℤ} {r : ℚ} (hn : Squarefree n) (hnr : ∃ (m : ℤ), ↑n * r ^ 2 = ↑m) : ∃ (t : ℤ), ↑t = r

theorem QuadraticInteger.two_b_int {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) : ∃ (B₂ : ℤ), ↑B₂ = 2 * b

theorem QuadraticInteger.b_int_of_a_int {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) (ha : ∃ (A : ℤ), ↑A = a) : ∃ (B : ℤ), ↑B = b

theorem QuadraticInteger.e_spec {d : ℤ} [h : Fact (d ≡ 1 [ZMOD 4])] : 4 * ((d - 1) / 4) = d - 1

theorem QuadraticInteger.algebra_S_K {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] [h : Fact (d ≡ 1 [ZMOD 4])] : (1 + QuadraticAlgebra.omega) / 2 * ((1 + QuadraticAlgebra.omega) / 2) = ((d - 1) / 4) • 1 + 1 • ((1 + QuadraticAlgebra.omega) / 2)

theorem QuadraticInteger.algebraMap_S_K_omega {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] [h : Fact (d ≡ 1 [ZMOD 4])] : (algebraMap (QuadraticAlgebra ℤ ((d - 1) / 4) 1) (QuadraticAlgebra ℚ (↑d) 0)) QuadraticAlgebra.omega = 2⁻¹ * (QuadraticAlgebra.omega + 1)

theorem QuadraticInteger.easy_incl_d_1 {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] [h : Fact (d ≡ 1 [ZMOD 4])] : IsIntegral ℤ ((algebraMap (QuadraticAlgebra ℤ ((d - 1) / 4) 1) (QuadraticAlgebra ℚ (↑d) 0)) QuadraticAlgebra.omega)

theorem QuadraticInteger.d_1_int {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] [h : Fact (d ≡ 1 [ZMOD 4])] {a b : ℚ} (hz : IsIntegral ℤ (↑a + b • QuadraticAlgebra.omega)) (ha : ∃ (A : ℤ), ↑A = a) : ↑a + b • QuadraticAlgebra.omega ∈ Set.range ⇑(algebraMap (QuadraticAlgebra ℤ ((d - 1) / 4) 1) (QuadraticAlgebra ℚ (↑d) 0))

theorem QuadraticInteger.d_1 {d : ℤ} [sf : Fact (Squarefree d)] [alt : d.natAbs.AtLeastTwo] [h : Fact (d ≡ 1 [ZMOD 4])] : IsIntegralClosure (QuadraticAlgebra ℤ ((d - 1) / 4) 1) ℤ (QuadraticAlgebra ℚ (↑d) 0)