Commit 2025-02-18 10:05 6d69b89e

View on Github →

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

Estimated changes

Modified Mathlib/Logic/Equiv/List.lean

added def Equiv.listUniqueEquiv

modified def Equiv.listUnitEquiv