equal
deleted
inserted
replaced
319 by (rule order_trans [OF _ norm_ge_zero], simp) |
319 by (rule order_trans [OF _ norm_ge_zero], simp) |
320 |
320 |
321 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a" |
321 lemma complex_mod_triangle_ineq2 [simp]: "cmod(b + a) - cmod b \<le> cmod a" |
322 by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) |
322 by (rule ord_le_eq_trans [OF norm_triangle_ineq2], simp) |
323 |
323 |
324 lemmas real_sum_squared_expand = power2_sum [where 'a=real] |
|
325 |
|
326 lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x" |
324 lemma abs_Re_le_cmod: "\<bar>Re x\<bar> \<le> cmod x" |
327 by (cases x) simp |
325 by (cases x) simp |
328 |
326 |
329 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
327 lemma abs_Im_le_cmod: "\<bar>Im x\<bar> \<le> cmod x" |
330 by (cases x) simp |
328 by (cases x) simp |