| author | wenzelm |
| Fri, 20 Oct 2023 22:19:05 +0200 | |
| changeset 78805 | 62616d8422c5 |
| parent 77406 | c2013f617a70 |
| child 80084 | 173548e4d5d0 |
| permissions | -rw-r--r-- |
| 68582 | 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 | 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 |
|
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
8 |
end |