Commit 2023-01-30 02:58 1246b7b8

View on Github →

feat: Port Data.Finsupp.NeLocus (#1935)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/NeLocus.lean

added theorem Finsupp.coe_neLocus

added theorem Finsupp.mapRange_neLocus_eq

added theorem Finsupp.mem_neLocus

added def Finsupp.neLocus

added theorem Finsupp.neLocus_add_left

added theorem Finsupp.neLocus_add_right

added theorem Finsupp.neLocus_comm

added theorem Finsupp.neLocus_eq_empty

added theorem Finsupp.neLocus_eq_support_sub

added theorem Finsupp.neLocus_neg

added theorem Finsupp.neLocus_neg_neg

added theorem Finsupp.neLocus_self_add_left

added theorem Finsupp.neLocus_self_add_right

added theorem Finsupp.neLocus_self_sub_left

added theorem Finsupp.neLocus_self_sub_right

added theorem Finsupp.neLocus_sub_left

added theorem Finsupp.neLocus_sub_right

added theorem Finsupp.neLocus_zero_left

added theorem Finsupp.neLocus_zero_right

added theorem Finsupp.nonempty_neLocus_iff

added theorem Finsupp.not_mem_neLocus

added theorem Finsupp.subset_mapRange_neLocus

added theorem Finsupp.zipWith_neLocus_eq_left

added theorem Finsupp.zipWith_neLocus_eq_right