Finsupp

📁 Source: Mathlib/Data/Finset/Finsupp.lean

Statistics

Metric	Count
Definitions finsupp, pi	2
Theorems card_finsupp, mem_finsupp_iff, mem_finsupp_iff_of_support_subset, card_pi, mem_pi	5
Total	7

Finset

Definitions

Name	Category	Theorems
finsupp 📖	CompOp	4 math math: mem_finsupp_iff, mem_finsupp_iff_of_support_subset, Finsupp.Icc_eq, card_finsupp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_finsupp 📖	mathematical	—	card Finsupp finsupp prod Nat.instCommMonoid	—	Finsupp.indicator_injective card_map card_pi
mem_finsupp_iff 📖	mathematical	—	Finsupp Finset SetLike.instMembership instSetLike finsupp instHasSubset Finsupp.support DFunLike.coe Finsupp.instFunLike	—	Finsupp.indicator_injective mem_map Finsupp.support_indicator_subset Finsupp.indicator_of_mem mem_pi Finsupp.ext Finsupp.notMem_support_iff
mem_finsupp_iff_of_support_subset 📖	mathematical	Finset instHasSubset Finsupp.support zero	Finsupp Finset SetLike.instMembership instSetLike finsupp DFunLike.coe zero Finsupp.instFunLike	—	mem_finsupp_iff Finsupp.notMem_support_iff zero_mem_zero Finsupp.mem_support_iff mem_zero

Finsupp

Definitions

Name	Category	Theorems
pi 📖	CompOp	2 math math: card_pi, mem_pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_pi 📖	mathematical	—	Finset.card Finsupp pi prod Finset Finset.zero Nat.instCommMonoid Pi.instNatCast DFunLike.coe instFunLike	—	pi.eq_1 Finset.card_finsupp Finset.prod_congr
mem_pi 📖	mathematical	—	Finsupp Finset SetLike.instMembership Finset.instSetLike pi DFunLike.coe Finset.zero instFunLike	—	Finset.mem_finsupp_iff_of_support_subset Finset.Subset.refl

---

← Back to Index