Commit 2023-01-19 07:29 73aea12b

View on Github →

feat: port Data.List.NodupEquivFin (#1640)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/NodupEquivFin.lean

added def List.Nodup.getBijectionOfForallMemList

added def List.Nodup.getEquiv

added def List.Nodup.getEquivOfForallMemList

added theorem List.Sorted.coe_getIso_apply

added theorem List.Sorted.coe_getIso_symm_apply

added def List.Sorted.getIso

added theorem List.Sorted.get_mono

added theorem List.Sorted.get_strictMono

added theorem List.duplicate_iff_exists_distinct_get

added theorem List.duplicate_iff_exists_distinct_nthLe

added theorem List.sublist_iff_exists_fin_orderEmbedding_get_eq

added theorem List.sublist_iff_exists_orderEmbedding_get?_eq

added theorem List.sublist_of_orderEmbedding_get?_eq