Mathlib Changelog
v4
Changelog
About
Github
Def
invertibleOfLeftInverse
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
invertibleOfLeftInverse
View on Github →