Theorem Equiv.Perm.AddAut.coe_inv

Modification history

2026-05-27 15:09
Mathlib/Algebra/Group/End.lean
refactor(GroupTheory/*): additivize `AddAut` (#39884) …
Deleted Equiv.Perm.AddAut.coe_invView on Github →
2025-05-13 13:05
Mathlib/Algebra/Group/End.lean
feat(Algebra/Group/End) : add MulAut.inv_apply and some simp lemmas (#24082)
Added Equiv.Perm.AddAut.coe_invView on Github →