equal
deleted
inserted
replaced
68 |
68 |
69 primcorec inverse_complex where |
69 primcorec inverse_complex where |
70 "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" |
70 "Re (inverse x) = Re x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" |
71 | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" |
71 | "Im (inverse x) = - Im x / ((Re x)\<^sup>2 + (Im x)\<^sup>2)" |
72 |
72 |
73 definition "x div (y\<Colon>complex) = x * inverse y" |
73 definition "x div (y::complex) = x * inverse y" |
74 |
74 |
75 instance |
75 instance |
76 by intro_classes |
76 by intro_classes |
77 (simp_all add: complex_eq_iff divide_complex_def |
77 (simp_all add: complex_eq_iff divide_complex_def |
78 distrib_left distrib_right right_diff_distrib left_diff_distrib |
78 distrib_left distrib_right right_diff_distrib left_diff_distrib |