equal
deleted
inserted
replaced
585 |
585 |
586 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)" |
586 lemma cis_inverse [simp]: "inverse(cis a) = cis (-a)" |
587 by (simp add: cis_def) |
587 by (simp add: cis_def) |
588 |
588 |
589 lemma cis_divide: "cis a / cis b = cis (a - b)" |
589 lemma cis_divide: "cis a / cis b = cis (a - b)" |
590 by (simp add: complex_divide_def cis_mult diff_minus) |
590 by (simp add: complex_divide_def cis_mult) |
591 |
591 |
592 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" |
592 lemma cos_n_Re_cis_pow_n: "cos (real n * a) = Re(cis a ^ n)" |
593 by (auto simp add: DeMoivre) |
593 by (auto simp add: DeMoivre) |
594 |
594 |
595 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" |
595 lemma sin_n_Im_cis_pow_n: "sin (real n * a) = Im(cis a ^ n)" |