isabelle: src/HOL/Algebra/abstract/Factor.thy@b5eca86ef9cc (annotated)

7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	1	(*
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	2	Factorisation within a factorial domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	3	$Id$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	4	Author: Clemens Ballarin, started 25 November 1997
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	5	*)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	6
20318 0e0ea63fe768 Restructured algebra library, added ideals and quotient rings. ballarin parents: 17479 diff changeset	7	theory Factor imports Ring2 begin
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	8
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	9	constdefs
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	10	Factorisation :: "['a::ring, 'a list, 'a] => bool"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	11	(* factorisation of x into a list of irred factors and a unit u *)
17479 68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	12	"Factorisation x factors u ==
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	13	x = foldr op* factors u &
68a7acb5f22e converted to Isar theory format; wenzelm parents: 13735 diff changeset	14	(ALL a : set factors. irred a) & u dvd 1"
7998 3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	15
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin paulson parents: diff changeset	16	end

author	wenzelm
	Thu, 03 Aug 2006 17:30:43 +0200
changeset 20335	b5eca86ef9cc
parent 20318	0e0ea63fe768
child 21423	6cdd0589aa73
permissions	-rw-r--r--