equal
deleted
inserted
replaced
1 (* |
1 (* Author: Clemens Ballarin, started 25 November 1997 |
2 Factorisation within a factorial domain |
2 |
3 $Id$ |
3 Factorisation within a factorial domain. |
4 Author: Clemens Ballarin, started 25 November 1997 |
|
5 *) |
4 *) |
6 |
5 |
7 theory Factor imports Ring2 begin |
6 theory Factor |
|
7 imports Ring2 |
|
8 begin |
8 |
9 |
9 definition |
10 definition |
10 Factorisation :: "['a::ring, 'a list, 'a] => bool" where |
11 Factorisation :: "['a::ring, 'a list, 'a] => bool" where |
11 (* factorisation of x into a list of irred factors and a unit u *) |
12 (* factorisation of x into a list of irred factors and a unit u *) |
12 "Factorisation x factors u \<longleftrightarrow> |
13 "Factorisation x factors u \<longleftrightarrow> |