Def Equiv.listUnitEquiv

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)

Modified Equiv.listUnitEquiv View on Github →

2023-01-20 10:06

Mathlib/Logic/Equiv/List.lean

feat: port Logic.Equiv.List (#1709)

Added Equiv.listUnitEquiv View on Github →