Theory New_Algebra

section ‹The New-Algebra Development›

theory New_Algebra
  imports
    (* groups *)
    Subgroup_Lattice
    Monoid_Iso_Classes
    Normal_Series
    Normal_Chain
    Group_Product
    Group_Family_Product
    Schreier_Refinement
    Simple_Factor_Chain
    Jordan_Hoelder_Uniqueness
    Maximal_Normal_Subgroup
    Finite_Composition_Series
    Sn_Composition_Factors
    Abel_Ruffini
    P_Group
    (* rings, ideals, divisibility *)
    Subring_Generated
    Finite_Field_Frobenius
    Ideal_Extension
    Chinese_Remainder_Rings
    Field_Of_Fractions
    Poly_Divisibility
    Closure_Algebraic
    (* modules and vector spaces *)
    Module_Complements
    Module_Exact_Sequence
    Module_Family_Product
    Free_Module_Universal
    Finite_Dimensional_Isomorphism
    Finite_Dimensional_Splitting
    (* fields, extensions, Galois theory *)
    Field_Extension
    Field_Mult_Cyclic
    Galois_Restriction_Splitting
    Galois_Finite_Correspondence
    Normal_Closure
    (* finite fields *)
    Finite_Field_Galois
    GF_p
begin

end