Commit 2023-01-30 06:43 c9524b66

View on Github →

feat: Port Data.Dfinsupp.NeLocus (#1937)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Dfinsupp/NeLocus.lean

added theorem Dfinsupp.coe_neLocus

added theorem Dfinsupp.mapRange_neLocus_eq

added theorem Dfinsupp.mem_neLocus

added def Dfinsupp.neLocus

added theorem Dfinsupp.neLocus_add_left

added theorem Dfinsupp.neLocus_add_right

added theorem Dfinsupp.neLocus_comm

added theorem Dfinsupp.neLocus_eq_empty

added theorem Dfinsupp.neLocus_eq_support_sub

added theorem Dfinsupp.neLocus_neg

added theorem Dfinsupp.neLocus_neg_neg

added theorem Dfinsupp.neLocus_self_add_left

added theorem Dfinsupp.neLocus_self_add_right

added theorem Dfinsupp.neLocus_self_sub_left

added theorem Dfinsupp.neLocus_self_sub_right

added theorem Dfinsupp.neLocus_sub_left

added theorem Dfinsupp.neLocus_sub_right

added theorem Dfinsupp.neLocus_zero_left

added theorem Dfinsupp.neLocus_zero_right

added theorem Dfinsupp.nonempty_neLocus_iff

added theorem Dfinsupp.not_mem_neLocus

added theorem Dfinsupp.subset_mapRange_neLocus

added theorem Dfinsupp.zipWith_neLocus_eq_left

added theorem Dfinsupp.zipWith_neLocus_eq_right