ring
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ (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