Theorem MulOneClass.isUnital

Modification history

2026-08-20 19:44

Mathlib/Algebra/Group/Defs.lean

refactor(Algebra/Group): split overlong file Defs.lean (#42952) …

Modified MulOneClass.isUnital View on Github →

2026-08-13 09:59

Mathlib/Algebra/Group/Defs.lean

feat(Algebra): `IsUnital` and `IsNotUnital` classes (#41923) …

Added MulOneClass.isUnital View on Github →