Commit 2023-04-10 18:54 16b5e0a3

View on Github →

feat: port Data.List.ToFinsupp (#3350)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/ToFinsupp.lean

added theorem List.coe_toFinsupp

added def List.toFinsupp

added theorem List.toFinsupp_append

added theorem List.toFinsupp_apply

added theorem List.toFinsupp_apply_fin

added theorem List.toFinsupp_apply_le

added theorem List.toFinsupp_apply_lt'

added theorem List.toFinsupp_apply_lt

added theorem List.toFinsupp_concat_eq_toFinsupp_add_single

added theorem List.toFinsupp_cons_apply_succ

added theorem List.toFinsupp_cons_apply_zero

added theorem List.toFinsupp_cons_eq_single_add_embDomain

added theorem List.toFinsupp_eq_sum_map_enum_single

added theorem List.toFinsupp_nil

added theorem List.toFinsupp_singleton

added theorem List.toFinsupp_support