Theorem ConjAct.toConjAct_smul_eq_mulAut_conj

Modification history

2026-03-12 12:09
Mathlib/GroupTheory/GroupAction/ConjAct.lean
feat(GroupTheory/SpecificGroups/Alternating/Simple): the alternating group on at least 5 letters is simple. (#33082) …
Added ConjAct.toConjAct_smul_eq_mulAut_conjView on Github →