theorem Zsqrtd.associated_norm_of_associated {d : ℤ} {f : ℤ√d} {g : ℤ√d} (h : Associated f g) : Associated (Zsqrtd.norm f) (Zsqrtd.norm g)

theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour (Zsqrtd.norm p)) (hcoprime : IsCoprime p.re p.im) : p.im ≠ 0

theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ |z.re| = 1 ∧ z.im = 0

theorem Zsqrt3.coe_of_isUnit {z : ℤ√(-3)} (h : IsUnit z) : ∃ u, z = ↑↑u

theorem Zsqrt3.coe_of_isUnit' {z : ℤ√(-3)} (h : IsUnit z) : ∃ u, z = ↑u ∧ |u| = 1

theorem OddPrimeOrFour.factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hx : OddPrimeOrFour x) (hfactor : x ∣ Zsqrtd.norm a) : ∃ c, |x| = Zsqrtd.norm c ∧ 0 ≤ c.re ∧ c.im ≠ 0

theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even (Zsqrtd.norm a)) : Odd a.re ∧ Odd a.im

theorem step1 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even (Zsqrtd.norm a)) : ∃ u, a = { re := 1, im := 1 } * u ∨ a = { re := 1, im := -1 } * u

theorem step1' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even (Zsqrtd.norm a)) : ∃ u, IsCoprime u.re u.im ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u

theorem step1'' {a : ℤ√(-3)} {p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hp : Zsqrtd.norm p = 4) (hq : p.im ≠ 0) (heven : Even (Zsqrtd.norm a)) : ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = 4 * Zsqrtd.norm u

theorem step2 {a : ℤ√(-3)} {p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a) (hpprime : Prime (Zsqrtd.norm p)) : ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u

theorem step1_2 {a : ℤ√(-3)} {p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : Zsqrtd.norm p ∣ Zsqrtd.norm a) (hp : OddPrimeOrFour (Zsqrtd.norm p)) (hq : p.im ≠ 0) : ∃ u, IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ Zsqrtd.norm a = Zsqrtd.norm p * Zsqrtd.norm u

theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : Zsqrtd.norm a ≠ 1) (hcoprime : IsCoprime a.re a.im) : ∃ u q, 0 ≤ q.re ∧ q.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm q) ∧ a = q * u ∧ IsCoprime u.re u.im ∧ Zsqrtd.norm u < Zsqrtd.norm a

theorem step3 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : ∃ f, (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧ ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)

theorem step4_3 {p : ℤ√(-3)} {p' : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hcoprime' : IsCoprime p'.re p'.im) (h : OddPrimeOrFour (Zsqrtd.norm p)) (heq : Zsqrtd.norm p = Zsqrtd.norm p') : |p.re| = |p'.re| ∧ |p.im| = |p'.im|

theorem prod_map_norm {d : ℤ} {s : Multiset (ℤ√d)} : Multiset.prod (Multiset.map Zsqrtd.norm s) = Zsqrtd.norm (Multiset.prod s)

theorem factors_unique_prod {f : Multiset (ℤ√(-3))} {g : Multiset (ℤ√(-3))} : (∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)) → (∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)) → Associated (Zsqrtd.norm (Multiset.prod f)) (Zsqrtd.norm (Multiset.prod g)) → Multiset.Rel Associated (Multiset.map Zsqrtd.norm f) (Multiset.map Zsqrtd.norm g)

noncomputable def factorization' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : Multiset (ℤ√(-3))

The multiset of factors.

Equations

• One or more equations did not get rendered due to their size.

theorem factorization'_prop {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : (a = Multiset.prod (factorization' hcoprime) ∨ a = -Multiset.prod (factorization' hcoprime)) ∧ ∀ (pq : ℤ√(-3)), pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)

theorem factorization'.coprime_of_mem {a : ℤ√(-3)} {b : ℤ√(-3)} (h : IsCoprime a.re a.im) (hmem : b ∈ factorization' h) : IsCoprime b.re b.im

theorem no_conj (s : Multiset (ℤ√(-3))) {p : ℤ√(-3)} (hp : ¬IsUnit p) (hcoprime : IsCoprime (Multiset.prod s).re (Multiset.prod s).im) : ¬(p ∈ s ∧ star p ∈ s)

def Associated' (x : ℤ√(-3)) (y : ℤ√(-3)) : Prop

Associated elements in ℤ√-3.

Equations

• Associated' x y = (Associated x y ∨ Associated x (star y))

theorem Associated'.refl (x : ℤ√(-3)) : Associated' x x

theorem Associated'.norm_eq {x : ℤ√(-3)} {y : ℤ√(-3)} (h : Associated' x y) : Zsqrtd.norm x = Zsqrtd.norm y

theorem associated'_of_abs_eq {x : ℤ√(-3)} {y : ℤ√(-3)} (hre : |x.re| = |y.re|) (him : |x.im| = |y.im|) : Associated' x y

theorem associated'_of_associated_norm {x : ℤ√(-3)} {y : ℤ√(-3)} (h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)) (hx : IsCoprime x.re x.im) (hy : IsCoprime y.re y.im) (h' : OddPrimeOrFour (Zsqrtd.norm x)) : Associated' x y

theorem factorization'.associated'_of_norm_eq {a : ℤ√(-3)} {b : ℤ√(-3)} {c : ℤ√(-3)} (h : IsCoprime a.re a.im) (hbmem : b ∈ factorization' h) (hcmem : c ∈ factorization' h) (hnorm : Zsqrtd.norm b = Zsqrtd.norm c) : Associated' b c

theorem factors_unique {f : Multiset (ℤ√(-3))} {g : Multiset (ℤ√(-3))} (hf : ∀ (x : ℤ√(-3)), x ∈ f → OddPrimeOrFour (Zsqrtd.norm x)) (hf' : ∀ (x : ℤ√(-3)), x ∈ f → IsCoprime x.re x.im) (hg : ∀ (x : ℤ√(-3)), x ∈ g → OddPrimeOrFour (Zsqrtd.norm x)) (hg' : ∀ (x : ℤ√(-3)), x ∈ g → IsCoprime x.re x.im) (h : Associated (Multiset.prod f) (Multiset.prod g)) : Multiset.Rel Associated' f g

theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : Even (evenFactorExp (Zsqrtd.norm a))

theorem factorsOddPrimeOrFour.unique {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) {f : Multiset ℤ} (hf : ∀ (x : ℤ), x ∈ f → OddPrimeOrFour x) (hf' : ∀ (x : ℤ), x ∈ f → 0 ≤ x) (hassoc : Associated (Multiset.prod f) (Zsqrtd.norm a)) : f = factorsOddPrimeOrFour (Zsqrtd.norm a)

theorem eq_or_eq_conj_of_associated_of_re_zero {x : ℤ√(-3)} {A : ℤ√(-3)} (hx : x.re = 0) (h : Associated x A) : x = A ∨ x = star A

theorem eq_or_eq_conj_iff_associated'_of_nonneg {x : ℤ√(-3)} {A : ℤ√(-3)} (hx : 0 ≤ x.re) (hA : 0 ≤ A.re) : Associated' x A ↔ x = A ∨ x = star A

theorem step5' (a : ℤ√(-3)) (r : ℤ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = Zsqrtd.norm a) : ∃ g, factorization' hcoprime = 3 • g

theorem step5 (a : ℤ√(-3)) (r : ℤ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = Zsqrtd.norm a) : ∃ p, a = p ^ 3

theorem step6 (a : ℤ) (b : ℤ) (r : ℤ) (hcoprime : IsCoprime a b) (hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2) : ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3