add lemma power_eq_imp_eq_base
authorhuffman
Sun May 13 19:15:36 2007 +0200 (2007-05-13)
changeset 2295548dc37776d1e
parent 22954 372e3471fca2
child 22956 617140080e6a
add lemma power_eq_imp_eq_base
src/HOL/Power.thy
     1.1 --- a/src/HOL/Power.thy	Sun May 13 18:16:49 2007 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun May 13 19:15:36 2007 +0200
     1.3 @@ -319,6 +319,11 @@
     1.4        ==> a = (b::'a::{ordered_semidom,recpower})"
     1.5  by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
     1.6  
     1.7 +lemma power_eq_imp_eq_base:
     1.8 +  fixes a b :: "'a::{ordered_semidom,recpower}"
     1.9 +  shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
    1.10 +by (cases n, simp_all, rule power_inject_base)
    1.11 +
    1.12  
    1.13  subsection{*Exponentiation for the Natural Numbers*}
    1.14