src/HOL/Analysis/Conformal_Mappings.thy
changeset 65578 e4997c181cce
parent 65538 a39ef48fbee0
child 65963 ca1e636fa716
     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Tue Apr 25 08:38:23 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Tue Apr 25 16:39:54 2017 +0100
     1.3 @@ -1244,7 +1244,7 @@
     1.4          by (meson Tsb min.cobounded1 order_trans r subset_ball)
     1.5        ultimately have False
     1.6          using inj_onD [OF injf, of y0 y1] \<open>y0 \<in> T\<close> \<open>y1 \<in> T\<close>
     1.7 -        using fd [of y0] fd [of y1] complex_root_unity [of n 1]
     1.8 +        using fd [of y0] fd [of y1] complex_root_unity [of n 1] n_ne
     1.9          apply (simp add: y0 y1 power_mult_distrib)
    1.10          apply (force simp: algebra_simps)
    1.11          done