exact HH.2
case h.e'_4.calc_1.hp
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
HH : |?m.81907.re| = 1 ∧ ?m.81907.im = 0
⊢ x.im = 0

a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour x.norm.natAbs
h : Associated x.norm A.norm
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ ℤ√(-3)
no goals