NeLocus

📁 Source: Mathlib/Data/DFinsupp/NeLocus.lean

Statistics

Metric	Count
Definitions neLocus	1
Theorems coe_neLocus, mapRange_neLocus_eq, mem_neLocus, neLocus_add_left, neLocus_add_right, neLocus_comm, neLocus_eq_empty, neLocus_eq_support_sub, neLocus_neg, neLocus_neg_neg, neLocus_self_add_left, neLocus_self_add_right, neLocus_self_sub_left, neLocus_self_sub_right, neLocus_sub_left, neLocus_sub_right, neLocus_zero_left, neLocus_zero_right, nonempty_neLocus_iff, notMem_neLocus, subset_mapRange_neLocus, zipWith_neLocus_eq_left, zipWith_neLocus_eq_right	23
Total	24

DFinsupp

Definitions

Name	Category	Theorems
neLocus 📖	CompOp	23 math math: neLocus_comm, neLocus_neg_neg, mem_neLocus, neLocus_self_sub_left, neLocus_self_add_right, neLocus_neg, neLocus_sub_left, zipWith_neLocus_eq_right, neLocus_self_sub_right, neLocus_zero_right, neLocus_sub_right, coe_neLocus, neLocus_add_right, notMem_neLocus, neLocus_eq_support_sub, neLocus_zero_left, neLocus_add_left, nonempty_neLocus_iff, neLocus_self_add_left, mapRange_neLocus_eq, zipWith_neLocus_eq_left, neLocus_eq_empty, subset_mapRange_neLocus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_neLocus 📖	mathematical	—	SetLike.coe Finset Finset.instSetLike neLocus setOf DFunLike.coe DFinsupp instDFunLike	—	Set.ext mem_neLocus
mapRange_neLocus_eq 📖	mathematical	—	neLocus mapRange	—	Finset.ext
mem_neLocus 📖	mathematical	—	Finset Finset.instMembership neLocus	—	Ne.ne_or_ne
neLocus_add_left 📖	mathematical	—	neLocus AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddLeftCancelMonoid.toAddMonoid DFinsupp instAdd	—	zipWith_neLocus_eq_left add_right_injective AddLeftCancelSemigroup.toIsLeftCancelAdd
neLocus_add_right 📖	mathematical	—	neLocus AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid DFinsupp instAdd	—	zipWith_neLocus_eq_right add_left_injective AddRightCancelSemigroup.toIsRightCancelAdd
neLocus_comm 📖	mathematical	—	neLocus	—	Finset.filter.congr_simp Finset.union_comm
neLocus_eq_empty 📖	mathematical	—	neLocus Finset Finset.instEmptyCollection	—	ext Iff.not mem_neLocus Finset.eq_empty_iff_forall_notMem Finset.filter.congr_simp Finset.filter_false
neLocus_eq_support_sub 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid support DFinsupp instSub	—	neLocus_add_right add_neg_cancel neLocus_zero_right sub_eq_add_neg
neLocus_neg 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instNeg	—	neLocus_neg_neg neg_neg
neLocus_neg_neg 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instNeg	—	mapRange_neLocus_eq neg_zero neg_injective
neLocus_self_add_left 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid support	—	neLocus_comm neLocus_self_add_right
neLocus_self_add_right 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instAdd AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid support	—	neLocus_zero_left neLocus_add_left add_zero
neLocus_self_sub_left 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instSub support	—	neLocus_comm neLocus_self_sub_right
neLocus_self_sub_right 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instSub support	—	sub_eq_add_neg neLocus_self_add_right support_neg
neLocus_sub_left 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instSub	—	neLocus.congr_simp sub_eq_add_neg neLocus_add_left neLocus_neg_neg
neLocus_sub_right 📖	mathematical	—	neLocus NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid DFinsupp instSub	—	neLocus.congr_simp sub_eq_add_neg neLocus_add_right
neLocus_zero_left 📖	mathematical	—	neLocus DFinsupp instZero support	—	neLocus_comm neLocus_zero_right
neLocus_zero_right 📖	mathematical	—	neLocus DFinsupp instZero support	—	Finset.ext mem_neLocus mem_support_iff coe_zero Pi.zero_apply
nonempty_neLocus_iff 📖	mathematical	—	Finset.Nonempty neLocus	—	Finset.nonempty_iff_ne_empty Iff.not neLocus_eq_empty
notMem_neLocus 📖	mathematical	—	Finset Finset.instMembership neLocus DFunLike.coe DFinsupp instDFunLike	—	Iff.not mem_neLocus not_ne_iff
subset_mapRange_neLocus 📖	mathematical	—	Finset Finset.instHasSubset neLocus mapRange	—	—
zipWith_neLocus_eq_left 📖	mathematical	—	neLocus zipWith	—	Finset.ext
zipWith_neLocus_eq_right 📖	mathematical	—	neLocus zipWith	—	Finset.ext

---

← Back to Index