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-Library.Disjoint_Sets
• 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
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Library.Countable_Set
• HOL-Library.Equipollence
• 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
• HOL-Library.Groups_Big_Fun
• HOL-Library.Fun_Lexorder
• HOL-Library.Poly_Mapping
• Free_Abelian_Groups
• HOL-Combinatorics.Cycles
• Solvable_Groups
• Sym_Groups
• Exact_Sequence
• Left_Coset
• SimpleGroups
• SndIsomorphismGrp
• Algebra