Theorems · Definition · group theory

MulAut.characteristic

{G : Type u_1} → [inst : Group G] → (H : Subgroup G) → [H.Characteristic] → MulAut G →* MulAut ↥H

If H is a characteristic subgroup of G, then every automorphism of G induces an automorphism of H.

Defined in

Mathlib.Algebra.Group.Subgroup.Basic

Cited by

2 results in Mathlib

Foundations

Depth 29 from the axioms · uses propext, Quot.sound

Assumes

GroupSubgroup.Characteristic