| author | kleing |
| Tue, 13 May 2003 08:59:21 +0200 | |
| changeset 14024 | 213dcc39358f |
| parent 13735 | 7de9342aca7a |
| child 17479 | 68a7acb5f22e |
| permissions | -rw-r--r-- |
(* Factorisation within a factorial domain $Id$ Author: Clemens Ballarin, started 25 November 1997 *) Factor = Ring + consts Factorisation :: ['a::ring, 'a list, 'a] => bool (* factorisation of x into a list of irred factors and a unit u *) defs Factorisation_def "Factorisation x factors u == x = foldr op* factors u & (ALL a : set factors. irred a) & u dvd 1" end