equal
deleted
inserted
replaced
14 (* Groups *) |
14 (* Groups *) |
15 |
15 |
16 use_thy "FiniteProduct"; (* Product operator for commutative groups *) |
16 use_thy "FiniteProduct"; (* Product operator for commutative groups *) |
17 use_thy "Sylow"; (* Sylow's theorem *) |
17 use_thy "Sylow"; (* Sylow's theorem *) |
18 use_thy "Bij"; (* Automorphism Groups *) |
18 use_thy "Bij"; (* Automorphism Groups *) |
|
19 use_thy "Lattice"; (* Lattices, and the complete lattice of subgroups *) |
19 |
20 |
20 (* Rings *) |
21 (* Rings *) |
21 |
22 |
22 use_thy "UnivPoly"; (* Rings and polynomials *) |
23 use_thy "UnivPoly"; (* Rings and polynomials *) |
23 |
24 |