menu

Set_Theory
Group_Theory
Order_Theory
Subgroup_Lattice
Monoid_Iso_Classes
Normal_Series
Normal_Chain
Group_Operations
Sylow_Theorems
Commutator
Solvable_Transfer
Group_Product
Group_Family_Product
Zassenhaus_Lemma
Schreier_Refinement
Simple_Factor_Chain
Jordan_Hoelder_Uniqueness
Maximal_Normal_Subgroup
Finite_Composition_Series
Composition_Factors_Solvable
Symmetric_Group
Sym_Not_Solvable
Symmetric_Generation
Sn_Composition_Factors
Subfield
Field_Extension_Tower
Simple_Extension
Iso_Extension
Ring_Theory
Galois_Automorphism
Complex_Field_Extension
Iso_Extension_Tower
Galois_Transitivity
Galois_Action
Action_To_Sn
Abel_Ruffini
P_Group
Subring_Generated
Characteristic
Finite_Composite
Poly_Ring
Ideal_Theory
Poly_Ideal
GF_p
Divisibility_Theory
Prime_Subfield
Module_Basics
Free_Module
Vector_Space
Steinitz
Field_Mult_Cyclic
Extension_Vector_Space
Finite_Field_Frobenius
Ideal_Lattice
Ideal_Extension
Ring_Family_Product
Chinese_Remainder_Rings
Field_Of_Fractions
Poly_Divisibility
Indexed_Poly
Closure_Extension
Poly_Typeclass
Extension_Degree
Finite_Extension
Algebraic_Transitivity
Extension_Properties
Finite_Extension_Tower
Finite_Generated_Extension
Linear_System
Closure_Algebraic
Module_Homomorphism
Quotient_Module
Module_First_Iso
Module_Iso_Theorems
Module_Complements
Module_Exact_Sequence
Module_Family_Product
Free_Module_Universal
Rank_Nullity
Finite_Dimensional_Isomorphism
Finite_Dimensional_Splitting
Field_Extension
Galois_Correspondence
Galois_Normality
Galois_Fixed_Field
Primitive_Element
Galois_Degree
Galois_Simple_Degree
Galois_Restriction
Galois_Restriction_Splitting
Artin
Artin_Degree
Galois_Finite_Correspondence
Radical_Extension
Normal_Closure
Finite_Field_Extensions
Finite_Field_Galois
New_Algebra

HOL-New_Algebra.Commutator

HTML Presentation