Def OneHom.inverse

Modification history

2024-11-22 09:37

Mathlib/Algebra/Group/Equiv/Basic.lean

chore: move def MonoidHom.inverse to earlier defs file (#19348) …

Modified OneHom.inverse View on Github →

2023-08-10 12:07

Mathlib/Algebra/Hom/Equiv/Basic.lean

chore: ensure all instances referred to directly have explicit names (#6423) …

Modified OneHom.inverse View on Github →

2023-07-24 10:54

Mathlib/Algebra/Hom/Equiv/Basic.lean

feat(Algebra.Ring.Equiv) : provide RingHom inverse (#5997) …

Added OneHom.inverse View on Github →