src/HOL/Library/Formal_Power_Series.thy
changeset 56480 093ea91498e6
parent 56479 91958d4b30f7
child 57129 7edb7550663e
     1.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 09 09:37:47 2014 +0200
     1.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Apr 09 09:37:48 2014 +0200
     1.3 @@ -2006,17 +2006,8 @@
     1.4  
     1.5  *)
     1.6  lemma eq_divide_imp':
     1.7 -  assumes c0: "(c::'a::field) \<noteq> 0"
     1.8 -    and eq: "a * c = b"
     1.9 -  shows "a = b / c"
    1.10 -proof -
    1.11 -  from eq have "a * c * inverse c = b * inverse c"
    1.12 -    by simp
    1.13 -  then have "a * (inverse c * c) = b/c"
    1.14 -    by (simp only: field_simps divide_inverse)
    1.15 -  then show "a = b/c"
    1.16 -    unfolding  field_inverse[OF c0] by simp
    1.17 -qed
    1.18 +  fixes c :: "'a::field" shows "c \<noteq> 0 \<Longrightarrow> a * c = b \<Longrightarrow> a = b / c"
    1.19 +  by (simp add: field_simps)
    1.20  
    1.21  lemma radical_unique:
    1.22    assumes r0: "(r (Suc k) (b$0)) ^ Suc k = b$0"