src/HOL/NthRoot.thy
changeset 62347 2230b7047376
parent 62131 1baed43f453e
child 62381 a6479cb85944
child 62390 842917225d56
     1.1 --- a/src/HOL/NthRoot.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Wed Feb 17 21:51:57 2016 +0100
     1.3 @@ -10,17 +10,6 @@
     1.4  imports Deriv Binomial
     1.5  begin
     1.6  
     1.7 -lemma abs_sgn_eq: "\<bar>sgn x :: real\<bar> = (if x = 0 then 0 else 1)"
     1.8 -  by (simp add: sgn_real_def)
     1.9 -
    1.10 -lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
    1.11 -  by (simp add: sgn_real_def)
    1.12 -
    1.13 -lemma power_eq_iff_eq_base:
    1.14 -  fixes a b :: "_ :: linordered_semidom"
    1.15 -  shows "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
    1.16 -  using power_eq_imp_eq_base[of a n b] by auto
    1.17 -
    1.18  subsection \<open>Existence of Nth Root\<close>
    1.19  
    1.20  text \<open>Existence follows from the Intermediate Value Theorem\<close>