src/HOL/Analysis/Complex_Analysis_Basics.thy
 changeset 69064 5840724b1d71 parent 68721 53ad5c01be3f child 69180 922833cc6839
```     1.1 --- a/src/HOL/Analysis/Complex_Analysis_Basics.thy	Sun Sep 23 21:49:31 2018 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Analysis_Basics.thy	Mon Sep 24 14:30:09 2018 +0200
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 "((( * ) c) has_derivative (( * ) c)) F"
1.8 +  shows "(((*) c) has_derivative ((*) c)) F"
1.9  by (rule has_derivative_mult_right [OF has_derivative_ident])
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 "( * ) 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 @@ -59,10 +59,10 @@
1.22    shows   "vector_derivative (\<lambda>z. cnj (f z)) (at x) = cnj (vector_derivative f (at x))"
1.23    using assms by (intro vector_derivative_cnj_within) auto
1.24
1.25 -lemma lambda_zero: "(\<lambda>h::'a::mult_zero. 0) = ( * ) 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) = ( * ) 1"
1.30 +lemma lambda_one: "(\<lambda>x::'a::monoid_mult. x) = (*) 1"
1.31    by auto
1.32
1.33  lemma uniformly_continuous_on_cmul_right [continuous_intros]:
1.34 @@ -283,7 +283,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]: "(( * ) 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 @@ -572,7 +572,7 @@
1.44    finally show ?thesis .
1.45  qed
1.46
1.47 -lemma analytic_on_linear [analytic_intros,simp]: "(( * ) 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 @@ -905,9 +905,9 @@
1.53      by (intro has_field_derivative_series[of S f f' g' x0] assms A has_field_derivative_at_within)
1.54    then obtain g where g: "\<And>x. x \<in> S \<Longrightarrow> (\<lambda>n. f n x) sums g x"
1.55      "\<And>x. x \<in> S \<Longrightarrow> (g has_field_derivative g' x) (at x within S)" by blast
1.56 -  from g(2)[OF x] have g': "(g has_derivative ( * ) (g' x)) (at x)"
1.57 +  from g(2)[OF x] have g': "(g has_derivative (*) (g' x)) (at x)"
1.58      by (simp add: has_field_derivative_def S)
1.59 -  have "((\<lambda>x. \<Sum>n. f n x) has_derivative ( * ) (g' x)) (at x)"
1.60 +  have "((\<lambda>x. \<Sum>n. f n x) has_derivative (*) (g' x)) (at x)"
1.61      by (rule has_derivative_transform_within_open[OF g' \<open>open S\<close> x])
1.62         (insert g, auto simp: sums_iff)
1.63    thus "(\<lambda>x. \<Sum>n. f n x) field_differentiable (at x)" unfolding differentiable_def
```