HOL-Algebra

README

Congruence

Order

Lattice

Complete_Lattice

Galois_Connection

Group

FiniteProduct

Coset

Exponent

Sylow

Bij

Ring

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

Solvable_Groups

Sym_Groups

Exact_Sequence

Ring_Divisibility

Polynomials

Polynomial_Divisibility

Indexed_Polynomials

Finite_Extensions

Algebraic_Closure

Left_Coset

SimpleGroups

SndIsomorphismGrp

Algebra