author | wenzelm |
Tue, 05 Nov 2019 14:28:00 +0100 | |
changeset 71047 | 87c132cf5860 |
parent 70160 | 8e9100dcde52 |
child 77089 | b4f892d0625d |
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 |
68569
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
6 |
begin |
c64319959bab
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
paulson <lp15@cam.ac.uk>
parents:
diff
changeset
|
7 |
end |