| changeset 66453 | cc19f7ca2ed6 |
| parent 66276 | acc3b7dd0b21 |
| child 66938 | c78ff0aeba4c |
| 66452:450cefec7c11 | 66453:cc19f7ca2ed6 |
|---|---|
6 section \<open>Factorial (semi)rings\<close> |
6 section \<open>Factorial (semi)rings\<close> |
7 |
7 |
8 theory Factorial_Ring |
8 theory Factorial_Ring |
9 imports |
9 imports |
10 Main |
10 Main |
11 "~~/src/HOL/Library/Multiset" |
11 "HOL-Library.Multiset" |
12 begin |
12 begin |
13 |
13 |
14 subsection \<open>Irreducible and prime elements\<close> |
14 subsection \<open>Irreducible and prime elements\<close> |
15 |
15 |
16 (* TODO: Move ? *) |
16 (* TODO: Move ? *) |