Commit 2025-05-13 13:05 6e8cef9d

View on Github →

feat(Algebra/Group/End) : add MulAut.inv_apply and some simp lemmas (#24082)

Estimated changes

Modified Mathlib/Algebra/Group/End.lean

added theorem Equiv.Perm.AddAut.coe_inv

added theorem Equiv.Perm.AddAut.inv_apply

added theorem Equiv.Perm.AddAut.inv_symm

added theorem Equiv.Perm.AddAut.symm_inv

added theorem Equiv.Perm.MulAut.coe_inv

added theorem Equiv.Perm.MulAut.inv_apply

added theorem Equiv.Perm.MulAut.inv_symm

added theorem Equiv.Perm.MulAut.symm_inv

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean