Session HOL-Algebra

Theories

• 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
• Divisibility
• QuotRing
• IntRing
• Weak_Morphisms
• Ideal_Product
• Chinese_Remainder
• Subrings
• Generated_Rings
• Generated_Fields
• Product_Groups
• Free_Abelian_Groups
• Embedded_Algebras
• Cycles
• Solvable_Groups
• Sym_Groups
• Exact_Sequence
• Ring_Divisibility
• Polynomials
• Polynomial_Divisibility
• Indexed_Polynomials
• Finite_Extensions
• Algebraic_Closure
• Algebra