Theorem nonempty_unique

Modification history

2024-10-12 06:38

Mathlib/Logic/Unique.lean

chore(*): assume `[Nonempty α] [Subsingleton α]` instead of `Unique α` (#17670)

Added nonempty_unique View on Github →