## Stream: new members

### Topic: multiplication of complex number

#### Artizuiala G. (Mar 20 2022 at 20:51):

I'm trying to prove the multiplication law of complex number before I use it to proving other things.
for example, I have two complex number, x = a + bi, y = c + di, and w.t.s x * y = (ac - bd) + i (ad + bc).
sor far, I tried:

example : ∀ (x y : ℂ), (∃ (a b : ℤ), x = a + complex.I * b) → (∃ (c d : ℤ), y = c + complex.I * d) → (∃ (e f : ℤ), x * y = e + complex.I * f) :=
begin
intros x y,
intros hx hy,
obtain ⟨a, b, hx⟩ := hx,
obtain ⟨c, d, hy⟩ := hy,
-- w.t.s x * y = (a * c - b * d) + complex.I * (a * d + b * c)
use a * c - b * d, -- x = ↑a + complex.I * ↑b
use a * d + b * c, -- y = ↑c + complex.I * ↑d
have hxy : x * y = (↑a + complex.I * ↑b) * (↑c + complex.I * ↑d),
exact congr (congr_arg has_mul.mul hx) hy,
have h3 : (x * y).re = (x.re) * y.re - (x.im) * y.im,
exact complex.mul_re x y,
have h4 : (x * y).im = (x.re) * y.im + (x.im) * y.re,
exact complex.mul_im x y,
-- have h5 : x.re = a,
sorry,
end


I have no idea how to do next, any suggestions?

Last updated: Dec 20 2023 at 11:08 UTC