Built with
Alectryon. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl.
(** Theory *)
Require Export HoTT.Algebra.Groups.Group.
Require Export HoTT.Algebra.Groups.Subgroup.
Require Export HoTT.Algebra.Groups.QuotientGroup.
Require Export HoTT.Algebra.Groups.GrpPullback.
Require Export HoTT.Algebra.Groups.GroupCoeq.
Require Export HoTT.Algebra.Groups.FreeGroup.
Require Export HoTT.Algebra.Groups.FreeProduct.
Require Export HoTT.Algebra.Groups.Presentation.
Require Export HoTT.Algebra.Groups.ShortExactSequence.
Require Export HoTT.Algebra.Groups.Finite.
(** Examples *)