isabelle: src/HOL/Computational_Algebra/Computational_Algebra.thy@274b4edca859 (annotated)

65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	1
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	2	section \<open>Pieces of computational Algebra\<close>
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	3
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	4	theory Computational_Algebra
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	5	imports
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	6	Euclidean_Algorithm
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	7	Factorial_Ring
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	8	Formal_Power_Series
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	9	Fraction_Field
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	10	Fundamental_Theorem_Algebra
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	11	Normalized_Fraction
66276 acc3b7dd0b21 More material on powers for HOL-Computational_Algebra/HOL-Number_Theory eberlm <eberlm@in.tum.de> parents: 65417 diff changeset	12	Nth_Powers
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	13	Polynomial_FPS
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	14	Polynomial
66805 274b4edca859 Polynomial_Factorial does not depend on Field_as_Ring as such haftmann parents: 66276 diff changeset	15	Polynomial_Factorial
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	16	Primes
66276 acc3b7dd0b21 More material on powers for HOL-Computational_Algebra/HOL-Number_Theory eberlm <eberlm@in.tum.de> parents: 65417 diff changeset	17	Squarefree
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	18	begin
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	19
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	20	end
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	21

author	haftmann
	Sun, 08 Oct 2017 22:28:21 +0200
changeset 66805	274b4edca859
parent 66276	acc3b7dd0b21
child 67165	22a5822f52f7
permissions	-rw-r--r--