9.2. Properties of Groups
Morphisms and isomorphisms of groups exist and have a special notation as shown below:
variable (H : Type*) [Group H]
(f : G →* H) (e : G ≃* H)
Subgroups and quotients also exist. For example the following demonstrates that Mathlib knows that the cosets of a normal subgroup are naturally a group:
variable (N : Subgroup G) [N.Normal]
#synth Group (G ⧸ N)
Familiar concepts from group theory appear in Mathlib as follows:
-
Nilpotency
Group.IsNilpotent -
Solvability
IsSolvable -
Simplicity
IsSimpleGroup
as well as many more.