Theorems · Definition · group theory

MulAut.conj

{G : Type u_3} → [inst : Group G] → G →* MulAut G

Group conjugation, MulAut.conj g h = g * h * g⁻¹, as a monoid homomorphism mapping multiplication in G into multiplication in the automorphism group MulAut G. See also the type ConjAct G for any group G, which has a MulAction (ConjAct G) G instance where conj G acts on G by conjugation.

Defined in

Mathlib.Algebra.Group.End

Cited by

64 results in Mathlib

Foundations

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

Assumes

Group