ring
a : ℤ√(-3)
x : ℤ
hodd : Odd x
m c : ℤ
ha : c + m * x = a.re
hc : 2 * c.natAbs < x.natAbs
n d : ℤ
hb : d + n * x = a.im
hd : 2 * d.natAbs < x.natAbs
c' : ℤ√(-3) := { re := c, im := d }
⊢ 4 * (c'.re * c'.re - -3 * c'.im * c'.im) = (2 * c) ^ 2 + 3 * (2 * d) ^ 2
no goals