Theorems · Definition · group theory

MulAut.congr

{G : Type u_3} → [inst : Group G] → {H : Type u_7} → [inst_1 : Group H] → G ≃* H → MulAut G ≃* MulAut H

Isomorphic groups have isomorphic automorphism groups.

Defined in

Mathlib.Algebra.Group.End

Cited by

6 results in Mathlib

Foundations

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

Assumes

GroupGroup