Theorem IsRightRegular.subsingleton

Modification history

2025-06-24 10:56
Mathlib/Algebra/GroupWithZero/Regular.lean
refactor: move the definition of `IsRegular` earlier (#26321) …
Modified IsRightRegular.subsingletonView on Github →
2022-11-28 16:05
Mathlib/Algebra/Regular/Basic.lean
feat(Algebra/Regular/Basic): port file (#758) …
Added IsRightRegular.subsingletonView on Github →