unfold complexα
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
a b c : ℤα
x y : ℤ
⊢ ↑x + ↑y * { re := 1 / 2, im := rt7 / 2 } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }