Theorem subsingleton_iff_isEmpty_or_unique

Modification history

2026-10-17 11:31
Mathlib/Basic/Unique.lean
feat(FreeGroup): characterize commutative/cyclic free groups (#41988) …
Added subsingleton_iff_isEmpty_or_uniqueView on Github →