src/HOL/Power.thy
 changeset 23431 25ca91279a9b parent 23305 8ae6f7b0903b child 23544 4b4165cb3e0d
equal inserted replaced
23430:771117253634 23431:25ca91279a9b
`   331   show "z^(Suc n) = z * (z^n)" by simp`
`   331   show "z^(Suc n) = z * (z^n)" by simp`
`   332 qed`
`   332 qed`
`   333 `
`   333 `
`   334 lemma of_nat_power:`
`   334 lemma of_nat_power:`
`   335   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"`
`   335   "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"`
`   336 by (induct n, simp_all add: power_Suc)`
`   336 by (induct n, simp_all add: power_Suc of_nat_mult)`
`   337 `
`   337 `
`   338 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"`
`   338 lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"`
`   339 by (insert one_le_power [of i n], simp)`
`   339 by (insert one_le_power [of i n], simp)`
`   340 `
`   340 `
`   341 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"`
`   341 lemma nat_zero_less_power_iff [simp]: "(0 < x^n) = (x \<noteq> (0::nat) | n=0)"`