Def List.getEquivOfForallCountEqOne

Modification history

2025-11-04 13:39

Mathlib/Data/List/NodupEquivFin.lean

feat(Data/List/NodupEquivFin): add equiv with `count = 1` hypothesis (#30215)

Added List.getEquivOfForallCountEqOne View on Github →