Mathlib Changelog
v4
Changelog
About
Github
Def
invertibleOfRightInverse
Modification history
2025-12-12 12:04
Mathlib/Algebra/Group/Invertible/Defs.lean
feat(Algebra): define Dedekind-finite monoids (every left inverse is also a right inverse) (#32610) …
Added
invertibleOfRightInverse
View on Github →