| changeset 23047 | 17f7d831efe2 |
| parent 23046 | 12f35ece221f |
| child 23049 | 11607c283074 |
--- a/src/HOL/Hyperreal/NthRoot.thy Sun May 20 09:05:44 2007 +0200 +++ b/src/HOL/Hyperreal/NthRoot.thy Sun May 20 09:21:04 2007 +0200 @@ -37,6 +37,10 @@ thus ?thesis .. qed +(* Used by Integration/RealRandVar.thy in AFP *) +lemma realpow_pos_nth2: "(0::real) < a \<Longrightarrow> \<exists>r>0. r ^ Suc n = a" +by (blast intro: realpow_pos_nth) + text {* Uniqueness of nth positive root *} lemma realpow_pos_nth_unique: