equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 section \<open>Big sum and product over finite (non-empty) sets\<close> |
8 section \<open>Big sum and product over finite (non-empty) sets\<close> |
9 |
9 |
10 theory Groups_Big |
10 theory Groups_Big |
11 imports Finite_Set Power |
11 imports Power |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>Generic monoid operation over a set\<close> |
14 subsection \<open>Generic monoid operation over a set\<close> |
15 |
15 |
16 locale comm_monoid_set = comm_monoid |
16 locale comm_monoid_set = comm_monoid |