Session HOL-Algebra

Theories

• README
• Congruence
• Order
• Lattice
• Complete_Lattice
• Galois_Connection
• Group
• FiniteProduct
• Coset
• Exponent
• Sylow
• Bij
• Ring
  • File ‹ringsimp.ML›
• Module
• AbelCoset
• Ideal
• RingHom
• UnivPoly
• Generated_Groups
• Elementary_Groups
• Multiplicative_Group
• Group_Action
• Zassenhaus
• HOL-Combinatorics.Transposition
• HOL-Combinatorics.Permutations
• HOL-Combinatorics.List_Permutation
• Divisibility
• QuotRing
• IntRing
• Weak_Morphisms
• Ring_Divisibility
• Subrings
• Polynomials
• Embedded_Algebras
• Polynomial_Divisibility
• Indexed_Polynomials
• Finite_Extensions
• Algebraic_Closure
• Algebraic_Closure_Type
• Ideal_Product
• Chinese_Remainder
• Generated_Rings
• Generated_Fields
• Product_Groups
• HOL-Cardinals.Fun_More
• HOL-Cardinals.Order_Relation_More
• HOL-Cardinals.Wellfounded_More
• HOL-Cardinals.Wellorder_Relation
• HOL-Cardinals.Wellorder_Embedding
• HOL-Cardinals.Order_Union
• HOL-Cardinals.Wellorder_Constructions
• HOL-Cardinals.Cardinal_Order_Relation
• HOL-Cardinals.Cardinal_Arithmetic
• Free_Abelian_Groups
• HOL-Combinatorics.Cycles
• Solvable_Groups
• Sym_Groups
• Exact_Sequence
• Left_Coset
• SimpleGroups
• SndIsomorphismGrp
• Algebra