Group theory

Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Maša Žaucer, Andreas Källberg, Louis Wasserman, Ulrik Buchholtz, Victor Blanchi, Gregor Perčič and malarbol.

Created on 2022-03-12.
Last modified on 2025-04-24.

Modules in the group theory namespace

module group-theory where

open import group-theory.abelian-groups public
open import group-theory.abelianization-groups public
open import group-theory.addition-homomorphisms-abelian-groups public
open import group-theory.arithmetic-sequences-semigroups public
open import group-theory.automorphism-groups public
open import group-theory.cartesian-products-abelian-groups public
open import group-theory.cartesian-products-concrete-groups public
open import group-theory.cartesian-products-groups public
open import group-theory.cartesian-products-monoids public
open import group-theory.cartesian-products-semigroups public
open import group-theory.category-of-abelian-groups public
open import group-theory.category-of-concrete-groups public
open import group-theory.category-of-group-actions public
open import group-theory.category-of-groups public
open import group-theory.category-of-orbits-groups public
open import group-theory.category-of-semigroups public
open import group-theory.cayleys-theorem public
open import group-theory.centers-groups public
open import group-theory.centers-monoids public
open import group-theory.centers-semigroups public
open import group-theory.central-elements-groups public
open import group-theory.central-elements-monoids public
open import group-theory.central-elements-semigroups public
open import group-theory.centralizer-subgroups public
open import group-theory.characteristic-subgroups public
open import group-theory.commutative-monoids public
open import group-theory.commutator-subgroups public
open import group-theory.commutators-of-elements-groups public
open import group-theory.commuting-elements-groups public
open import group-theory.commuting-elements-monoids public
open import group-theory.commuting-elements-semigroups public
open import group-theory.commuting-squares-of-group-homomorphisms public
open import group-theory.concrete-group-actions public
open import group-theory.concrete-groups public
open import group-theory.concrete-monoids public
open import group-theory.congruence-relations-abelian-groups public
open import group-theory.congruence-relations-commutative-monoids public
open import group-theory.congruence-relations-groups public
open import group-theory.congruence-relations-monoids public
open import group-theory.congruence-relations-semigroups public
open import group-theory.conjugation public
open import group-theory.conjugation-concrete-groups public
open import group-theory.contravariant-pushforward-concrete-group-actions public
open import group-theory.cores-monoids public
open import group-theory.cyclic-groups public
open import group-theory.decidable-subgroups public
open import group-theory.dependent-products-abelian-groups public
open import group-theory.dependent-products-commutative-monoids public
open import group-theory.dependent-products-groups public
open import group-theory.dependent-products-monoids public
open import group-theory.dependent-products-semigroups public
open import group-theory.dihedral-group-construction public
open import group-theory.dihedral-groups public
open import group-theory.e8-lattice public
open import group-theory.elements-of-finite-order-groups public
open import group-theory.embeddings-abelian-groups public
open import group-theory.embeddings-groups public
open import group-theory.endomorphism-rings-abelian-groups public
open import group-theory.epimorphisms-groups public
open import group-theory.equivalences-concrete-group-actions public
open import group-theory.equivalences-concrete-groups public
open import group-theory.equivalences-group-actions public
open import group-theory.equivalences-semigroups public
open import group-theory.exponents-abelian-groups public
open import group-theory.exponents-groups public
open import group-theory.free-concrete-group-actions public
open import group-theory.free-groups-with-one-generator public
open import group-theory.full-subgroups public
open import group-theory.full-subsemigroups public
open import group-theory.function-abelian-groups public
open import group-theory.function-commutative-monoids public
open import group-theory.function-groups public
open import group-theory.function-monoids public
open import group-theory.function-semigroups public
open import group-theory.functoriality-quotient-groups public
open import group-theory.furstenberg-groups public
open import group-theory.generating-elements-groups public
open import group-theory.generating-sets-groups public
open import group-theory.group-actions public
open import group-theory.groups public
open import group-theory.homomorphisms-abelian-groups public
open import group-theory.homomorphisms-commutative-monoids public
open import group-theory.homomorphisms-concrete-group-actions public
open import group-theory.homomorphisms-concrete-groups public
open import group-theory.homomorphisms-generated-subgroups public
open import group-theory.homomorphisms-group-actions public
open import group-theory.homomorphisms-groups public
open import group-theory.homomorphisms-groups-equipped-with-normal-subgroups public
open import group-theory.homomorphisms-monoids public
open import group-theory.homomorphisms-semigroups public
open import group-theory.homotopy-automorphism-groups public
open import group-theory.images-of-group-homomorphisms public
open import group-theory.images-of-semigroup-homomorphisms public
open import group-theory.integer-multiples-of-elements-abelian-groups public
open import group-theory.integer-powers-of-elements-groups public
open import group-theory.intersections-subgroups-abelian-groups public
open import group-theory.intersections-subgroups-groups public
open import group-theory.inverse-semigroups public
open import group-theory.invertible-elements-monoids public
open import group-theory.isomorphisms-abelian-groups public
open import group-theory.isomorphisms-concrete-groups public
open import group-theory.isomorphisms-group-actions public
open import group-theory.isomorphisms-groups public
open import group-theory.isomorphisms-monoids public
open import group-theory.isomorphisms-semigroups public
open import group-theory.iterated-cartesian-products-concrete-groups public
open import group-theory.kernels-homomorphisms-abelian-groups public
open import group-theory.kernels-homomorphisms-concrete-groups public
open import group-theory.kernels-homomorphisms-groups public
open import group-theory.large-semigroups public
open import group-theory.loop-groups-sets public
open import group-theory.mere-equivalences-concrete-group-actions public
open import group-theory.mere-equivalences-group-actions public
open import group-theory.minkowski-multiplication-commutative-monoids public
open import group-theory.minkowski-multiplication-monoids public
open import group-theory.minkowski-multiplication-semigroups public
open import group-theory.monoid-actions public
open import group-theory.monoids public
open import group-theory.monomorphisms-concrete-groups public
open import group-theory.monomorphisms-groups public
open import group-theory.multiples-of-elements-abelian-groups public
open import group-theory.nontrivial-groups public
open import group-theory.normal-closures-subgroups public
open import group-theory.normal-cores-subgroups public
open import group-theory.normal-subgroups public
open import group-theory.normal-subgroups-concrete-groups public
open import group-theory.normal-submonoids public
open import group-theory.normal-submonoids-commutative-monoids public
open import group-theory.normalizer-subgroups public
open import group-theory.nullifying-group-homomorphisms public
open import group-theory.opposite-groups public
open import group-theory.opposite-semigroups public
open import group-theory.orbit-stabilizer-theorem-concrete-groups public
open import group-theory.orbits-concrete-group-actions public
open import group-theory.orbits-group-actions public
open import group-theory.orders-of-elements-groups public
open import group-theory.perfect-cores public
open import group-theory.perfect-groups public
open import group-theory.perfect-subgroups public
open import group-theory.powers-of-elements-commutative-monoids public
open import group-theory.powers-of-elements-groups public
open import group-theory.powers-of-elements-monoids public
open import group-theory.precategory-of-commutative-monoids public
open import group-theory.precategory-of-concrete-groups public
open import group-theory.precategory-of-group-actions public
open import group-theory.precategory-of-groups public
open import group-theory.precategory-of-monoids public
open import group-theory.precategory-of-orbits-monoid-actions public
open import group-theory.precategory-of-semigroups public
open import group-theory.principal-group-actions public
open import group-theory.principal-torsors-concrete-groups public
open import group-theory.products-of-elements-monoids public
open import group-theory.products-of-tuples-of-elements-commutative-monoids public
open import group-theory.pullbacks-subgroups public
open import group-theory.pullbacks-subsemigroups public
open import group-theory.quotient-groups public
open import group-theory.quotient-groups-concrete-groups public
open import group-theory.quotients-abelian-groups public
open import group-theory.rational-commutative-monoids public
open import group-theory.representations-monoids-precategories public
open import group-theory.saturated-congruence-relations-commutative-monoids public
open import group-theory.saturated-congruence-relations-monoids public
open import group-theory.semigroups public
open import group-theory.sheargroups public
open import group-theory.shriek-concrete-group-actions public
open import group-theory.stabilizer-groups public
open import group-theory.stabilizer-groups-concrete-group-actions public
open import group-theory.subgroups public
open import group-theory.subgroups-abelian-groups public
open import group-theory.subgroups-concrete-groups public
open import group-theory.subgroups-generated-by-elements-groups public
open import group-theory.subgroups-generated-by-families-of-elements-groups public
open import group-theory.subgroups-generated-by-subsets-groups public
open import group-theory.submonoids public
open import group-theory.submonoids-commutative-monoids public
open import group-theory.subsemigroups public
open import group-theory.subsets-abelian-groups public
open import group-theory.subsets-commutative-monoids public
open import group-theory.subsets-groups public
open import group-theory.subsets-monoids public
open import group-theory.subsets-semigroups public
open import group-theory.substitution-functor-concrete-group-actions public
open import group-theory.substitution-functor-group-actions public
open import group-theory.surjective-group-homomorphisms public
open import group-theory.surjective-semigroup-homomorphisms public
open import group-theory.symmetric-concrete-groups public
open import group-theory.symmetric-groups public
open import group-theory.torsion-elements-groups public
open import group-theory.torsion-free-groups public
open import group-theory.torsors public
open import group-theory.transitive-concrete-group-actions public
open import group-theory.transitive-group-actions public
open import group-theory.trivial-concrete-groups public
open import group-theory.trivial-group-homomorphisms public
open import group-theory.trivial-groups public
open import group-theory.trivial-subgroups public
open import group-theory.unordered-tuples-of-elements-commutative-monoids public
open import group-theory.wild-representations-monoids public

Recent changes