Commit 2024-11-22 09:37 944e3576

View on Github →

chore: move def MonoidHom.inverse to earlier defs file (#19348) No import effect, just moving defs to be with other defs.

Estimated changes

Modified Mathlib/Algebra/Group/Equiv/Basic.lean

deleted def MonoidHom.inverse

deleted def MulHom.inverse

deleted def OneHom.inverse

Modified Mathlib/Algebra/Group/Hom/Defs.lean

added def MonoidHom.inverse

added def MulHom.inverse

added def OneHom.inverse

Modified MathlibTest/symm.lean

deleted def MulHom.inverse