ring
case inr.intro.inr.intro
a : ℤ√(-3)
heven : Even (Zsqrtd.norm a)
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re = 4 * v + a.im
⊢ (4 * v + a.im) * (4 * v + a.im) - -3 * a.im * a.im = 4 * ((v + a.im) * (v + a.im) - -3 * v * v)
no goals