Automorphism groups
The automorphism group as an object: orders of automorphism groups, realizing groups as (outer) automorphism groups, class-preserving and inner automorphisms, automorphism orbits, endomorphism counts.
- Automorphism groups of p-groups
- Class-preserving automorphisms
- Endomorphisms and partial isomorphisms
- Groups as automorphism groups of relations
- Groups as outer automorphism groups
- One-relator groups as automorphism groups
- Orders of automorphism groups
- Outer automorphisms of poly-infinite-cyclic groups
DefinitionGroups with finitely many automorphism orbits#✓fully proved
MetaMathlibExt.HasFinitelyManyAutomorphismOrbits
A group \(G\) has finitely many automorphism orbits if the action of its automorphism group \(\operatorname{Aut}(G)\) on \(G\) has only finitely many orbits.
def HasFinitelyManyAutomorphismOrbits (G : Type*) [Group G] : Prop :=
Finite (MulAction.orbitRel.Quotient (MulAut G) G)Loading dependency explorer…
The dependency explorer needs JavaScript and its graph data.