Commit 2022-12-17 09:35 0ea857ef

View on Github →

feat: port Data.List.Func (#1048) aba57d4d3dae35460225919dcd82fe91355162f9

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/Func.lean

added def List.Func.Equiv

added def List.Func.add

added theorem List.Func.add_nil

added theorem List.Func.eq_get_of_mem

added theorem List.Func.eq_of_equiv

added theorem List.Func.equiv_of_eq

added theorem List.Func.equiv_refl

added theorem List.Func.equiv_symm

added theorem List.Func.equiv_trans

added theorem List.Func.forall_val_of_forall_mem

added def List.Func.get

added theorem List.Func.get_add

added theorem List.Func.get_eq_default_of_le

added theorem List.Func.get_map'

added theorem List.Func.get_map

added theorem List.Func.get_neg

added theorem List.Func.get_nil

added theorem List.Func.get_pointwise

added theorem List.Func.get_set

added theorem List.Func.get_set_eq_of_ne

added theorem List.Func.get_sub

added theorem List.Func.length_add

added theorem List.Func.length_neg

added theorem List.Func.length_pointwise

added theorem List.Func.length_set

added theorem List.Func.length_sub

added theorem List.Func.map_add_map

added theorem List.Func.mem_get_of_le

added theorem List.Func.mem_get_of_ne_zero

added def List.Func.neg

added theorem List.Func.nil_add

added theorem List.Func.nil_pointwise

added theorem List.Func.nil_sub

added def List.Func.pointwise

added theorem List.Func.pointwise_nil

added def List.Func.set

added def List.Func.sub

added theorem List.Func.sub_nil