isabelle: src/HOL/Algebra/Algebra.thy@29f2b8ff84f3 (annotated)

68582 b9b9e2985878 more standard headers; wenzelm parents: 68578 diff changeset	1	(* Title: HOL/Algebra/Algebra.thy *)
68569 c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena paulson <lp15@cam.ac.uk> parents: diff changeset	2
c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena paulson <lp15@cam.ac.uk> parents: diff changeset	3	theory Algebra
70063 adaa0a6ea4fe fixes for Free_Abelian_Groups paulson <lp15@cam.ac.uk> parents: 70040 diff changeset	4	imports Sylow Chinese_Remainder Zassenhaus Galois_Connection Generated_Fields Free_Abelian_Groups
70160 8e9100dcde52 Towards a proof of algebraic closure (NB not finished) paulson <lp15@cam.ac.uk> parents: 70063 diff changeset	5	Divisibility Embedded_Algebras IntRing Sym_Groups Exact_Sequence Polynomials Algebraic_Closure
77406 c2013f617a70 Importation of basic group theory results, due to Jakob von Raumer from his AFP entry Jordan-Hölder Theorem paulson <lp15@cam.ac.uk> parents: 77089 diff changeset	6	Left_Coset SimpleGroups SndIsomorphismGrp
68569 c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena paulson <lp15@cam.ac.uk> parents: diff changeset	7	begin
80084 173548e4d5d0 moved over material from the AFP to HOL, HOL-Computational_Algebra, and HOL-Number_Theory Manuel Eberl <manuel@pruvisto.org> parents: 77406 diff changeset	8
68569 c64319959bab Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena paulson <lp15@cam.ac.uk> parents: diff changeset	9	end

author	wenzelm
	Mon, 20 May 2024 15:43:51 +0200
changeset 80182	29f2b8ff84f3
parent 80084	173548e4d5d0
permissions	-rw-r--r--