src/HOL/Library/Fundamental_Theorem_Algebra.thy
changeset 59555 05573e5504a9
parent 58881 b9556a055632
child 59557 ebd8ecacfba6
     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:47 2015 +0100
     1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Wed Feb 18 22:46:48 2015 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4        using b v
     1.5        apply (simp add: th2)
     1.6        done
     1.7 -    from mult_less_imp_less_left[OF th4 th3]
     1.8 +    from mult_left_less_imp_less[OF th4 th3]
     1.9      have "?P ?w n" unfolding th1 .
    1.10      then have "\<exists>z. ?P z n" ..
    1.11    }