isabelle: src/HOL/Computational_Algebra/Computational_Algebra.thy@ff60b4acd6dd (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
69791 195aeee8b30a Formal Laurent series and overhaul of Formal power series (due to Jeremy Sylvestre) Manuel Eberl <eberlm@in.tum.de> parents: 67165 diff changeset	8	Formal_Laurent_Series
65417 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

author	paulson <lp15@cam.ac.uk>
	Tue, 01 Mar 2022 15:05:27 +0000
changeset 75168	ff60b4acd6dd
parent 70817	dd675800469d
permissions	-rw-r--r--