Mathlib Changelog
v4
Changelog
About
Github
Theorem
isLeftRegular_ofAdd
Modification history
2025-11-18 16:33
Mathlib/Algebra/Group/TypeTags/Basic.lean
feat: characterise regular elements of type synonyms (#31739)
Added
isLeftRegular_ofAdd
View on Github →