Def Equiv.listUniqueEquiv

Modification history

2025-02-18 10:05

Mathlib/Logic/Equiv/List.lean

feat(Logic/Equiv/List): lists on a unique type are equivalent to `ℕ` (#22017)

Added Equiv.listUniqueEquiv View on Github →