Commit 2023-01-18 08:36 0c21d424

View on Github →

feat: port Data.List.FinRange (#1635)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/FinRange.lean

added theorem Equiv.Perm.map_finRange_perm

added theorem Equiv.Perm.ofFn_comp_perm

added theorem List.finRange_succ_eq_map

added theorem List.map_coe_finRange

added theorem List.nodup_ofFn

added theorem List.nodup_ofFn_ofInjective

added theorem List.ofFn_eq_map

added theorem List.ofFn_eq_pmap

added theorem List.ofFn_id

Modified Mathlib/Data/List/Range.lean