isabelle: src/HOL/Computational_Algebra/Computational_Algebra.thy@851a9d9746c6 (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
67165 22a5822f52f7 dedicated theory for group closure haftmann parents: 66805 diff changeset	11	Group_Closure
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	12	Normalized_Fraction
66276 acc3b7dd0b21 More material on powers for HOL-Computational_Algebra/HOL-Number_Theory eberlm <eberlm@in.tum.de> parents: 65417 diff changeset	13	Nth_Powers
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	14	Polynomial_FPS
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	15	Polynomial
66805 274b4edca859 Polynomial_Factorial does not depend on Field_as_Ring as such haftmann parents: 66276 diff changeset	16	Polynomial_Factorial
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	17	Primes
66276 acc3b7dd0b21 More material on powers for HOL-Computational_Algebra/HOL-Number_Theory eberlm <eberlm@in.tum.de> parents: 65417 diff changeset	18	Squarefree
65417 fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	19	begin
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	20
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	21	end
fc41a5650fb1 session containing computational algebra haftmann parents: diff changeset	22

author	haftmann
	Wed, 22 Aug 2018 13:33:50 +0000
changeset 68790	851a9d9746c6
parent 67165	22a5822f52f7
child 69791	195aeee8b30a
permissions	-rw-r--r--