tuned spaces
authorblanchet
Fri Apr 04 14:44:51 2014 +0200 (2014-04-04)
changeset 56403ae4f904c98b0
parent 56402 6d9a24f87460
child 56404 9cb137ec6ec8
tuned spaces
src/HOL/Library/Fundamental_Theorem_Algebra.thy
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 04 13:22:26 2014 +0200
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Fri Apr 04 14:44:51 2014 +0200
     1.3 @@ -516,10 +516,10 @@
     1.4      {fix z::'a
     1.5        assume h: "(\<bar>d\<bar> + norm a) / norm c \<le> norm z"
     1.6        from c0 have "norm c > 0" by simp
     1.7 -      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z*c)"
     1.8 +      from h c0 have th0: "\<bar>d\<bar> + norm a \<le> norm (z * c)"
     1.9          by (simp add: field_simps norm_mult)
    1.10        have ath: "\<And>mzh mazh ma. mzh <= mazh + ma ==> abs(d) + ma <= mzh ==> d <= mazh" by arith
    1.11 -      from norm_diff_ineq[of "z*c" a ]
    1.12 +      from norm_diff_ineq[of "z * c" a ]
    1.13        have th1: "norm (z * c) \<le> norm (a + z * c) + norm a"
    1.14          by (simp add: algebra_simps)
    1.15        from ath[OF th1 th0] have "d \<le> norm (poly (pCons a (pCons c cs)) z)"
    1.16 @@ -720,7 +720,7 @@
    1.17        with norm_triangle_ineq[of "complex_of_real (1 - t^k)" "?w^k * ?w * poly s ?w"]
    1.18        have th11: "cmod (1 + ?w^k * (a + ?w * poly s ?w)) \<le> \<bar>1 - t^k\<bar> + cmod (?w^k * ?w * poly s ?w)" unfolding norm_of_real by simp
    1.19        have ath: "\<And>x (t::real). 0\<le> x \<Longrightarrow> x < t \<Longrightarrow> t\<le>1 \<Longrightarrow> \<bar>1 - t\<bar> + x < 1" by arith
    1.20 -      have "t *cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
    1.21 +      have "t * cmod w \<le> 1 * cmod w" apply (rule mult_mono) using t(1,2) by auto
    1.22        then have tw: "cmod ?w \<le> cmod w" using t(1) by (simp add: norm_mult)
    1.23        from t inv0 have "t* (cmod w ^ (k + 1) * m) < 1"
    1.24          by (simp add: inverse_eq_divide field_simps)
    1.25 @@ -1074,4 +1074,3 @@
    1.26    shows "poly [:c:] x = y \<longleftrightarrow> c = y" by simp
    1.27  
    1.28  end
    1.29 -