unfold toℂ
a b c : ℤα
x y : ℤ
⊢ toℂ { z := x, w := y } = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }
a b c : ℤα
x y : ℤ
⊢ ↑{ z := x, w := y }.z + ↑{ z := x, w := y }.w * complexα = { re := ↑x + ↑y / 2, im := ↑y * rt7 / 2 }