src/HOL/Analysis/Complex_Analysis_Basics.thy
changeset 67399 eab6ce8368fa
parent 67371 2d9cf74943e1
child 67968 a5ad4c015d1c
     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  lemma has_derivative_mult_right:
     1.6    fixes c:: "'a :: real_normed_algebra"
     1.7 -  shows "((op * c) has_derivative (op * c)) F"
     1.8 +  shows "((( * ) c) has_derivative (( * ) c)) F"
     1.9  by (rule has_derivative_mult_right [OF has_derivative_id])
    1.10  
    1.11  lemma has_derivative_of_real[derivative_intros, simp]:
    1.12 @@ -25,7 +25,7 @@
    1.13  
    1.14  lemma has_vector_derivative_real_field:
    1.15    "DERIV f (of_real a) :> f' \<Longrightarrow> ((\<lambda>x. f (of_real x)) has_vector_derivative f') (at a within s)"
    1.16 -  using has_derivative_compose[of of_real of_real a _ f "op * f'"]
    1.17 +  using has_derivative_compose[of of_real of_real a _ f "( * ) f'"]
    1.18    by (simp add: scaleR_conv_of_real ac_simps has_vector_derivative_def has_field_derivative_def)
    1.19  lemmas has_vector_derivative_real_complex = has_vector_derivative_real_field
    1.20  
    1.21 @@ -69,10 +69,10 @@
    1.22      shows  "b \<le> Im(l)"
    1.23    by (metis assms tendsto_le [OF _ _ tendsto_const]  tendsto_Im)
    1.24  
    1.25 -lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = op * 0"
    1.26 +lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 0"
    1.27    by auto
    1.28  
    1.29 -lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = op * 1"
    1.30 +lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = ( * ) 1"
    1.31    by auto
    1.32  
    1.33  lemma continuous_mult_left:
    1.34 @@ -315,7 +315,7 @@
    1.35  lemma holomorphic_cong: "s = t ==> (\<And>x. x \<in> s \<Longrightarrow> f x = g x) \<Longrightarrow> f holomorphic_on s \<longleftrightarrow> g holomorphic_on t"
    1.36    by (metis holomorphic_transform)
    1.37  
    1.38 -lemma holomorphic_on_linear [simp, holomorphic_intros]: "(op * c) holomorphic_on s"
    1.39 +lemma holomorphic_on_linear [simp, holomorphic_intros]: "(( * ) c) holomorphic_on s"
    1.40    unfolding holomorphic_on_def by (metis field_differentiable_linear)
    1.41  
    1.42  lemma holomorphic_on_const [simp, holomorphic_intros]: "(\<lambda>z. c) holomorphic_on s"
    1.43 @@ -570,7 +570,7 @@
    1.44    finally show ?thesis .
    1.45  qed
    1.46  
    1.47 -lemma analytic_on_linear [analytic_intros,simp]: "(op * c) analytic_on s"
    1.48 +lemma analytic_on_linear [analytic_intros,simp]: "(( * ) c) analytic_on s"
    1.49    by (auto simp add: analytic_on_holomorphic)
    1.50  
    1.51  lemma analytic_on_const [analytic_intros,simp]: "(\<lambda>z. c) analytic_on s"
    1.52 @@ -839,7 +839,7 @@
    1.53    show ?thesis
    1.54    unfolding has_field_derivative_def
    1.55    proof (rule has_derivative_sequence [OF cvs _ _ x])
    1.56 -    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (op * (f' n x))) (at x within s)"
    1.57 +    show "\<forall>n. \<forall>x\<in>s. (f n has_derivative (( * ) (f' n x))) (at x within s)"
    1.58        by (metis has_field_derivative_def df)
    1.59    next show "(\<lambda>n. f n x) \<longlonglongrightarrow> l"
    1.60      by (rule tf)
    1.61 @@ -906,9 +906,9 @@
    1.62    then obtain g where g: "\<And>x. x \<in> s \<Longrightarrow> (\<lambda>n. f n x) sums g x"
    1.63      "\<And>x. x \<in> s \<Longrightarrow> (g has_field_derivative g' x) (at x within s)" by blast
    1.64    from g[OF x] show "summable (\<lambda>n. f n x)" by (auto simp: summable_def)
    1.65 -  from g(2)[OF x] have g': "(g has_derivative op * (g' x)) (at x)"
    1.66 +  from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
    1.67      by (simp add: has_field_derivative_def s)
    1.68 -  have "((\<lambda>x. \<Sum>n. f n x) has_derivative op * (g' x)) (at x)"
    1.69 +  have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
    1.70      by (rule has_derivative_transform_within_open[OF g' \<open>open s\<close> x])
    1.71         (insert g, auto simp: sums_iff)
    1.72    thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def