equal
deleted
inserted
replaced
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header{*Exponentiation and Binomial Coefficients*} |
8 header{*Exponentiation and Binomial Coefficients*} |
9 |
9 |
10 theory Power = Divides: |
10 theory Power |
|
11 import Divides |
|
12 begin |
11 |
13 |
12 subsection{*Powers for Arbitrary Semirings*} |
14 subsection{*Powers for Arbitrary Semirings*} |
13 |
15 |
14 axclass recpower \<subseteq> comm_semiring_1_cancel, power |
16 axclass recpower \<subseteq> comm_semiring_1_cancel, power |
15 power_0 [simp]: "a ^ 0 = 1" |
17 power_0 [simp]: "a ^ 0 = 1" |