Sigma

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

Statistics

Metric	Count
Definitions embSigma	1
Theorems embSigma_add, embSigma_apply, embSigma_apply_of_ne, embSigma_apply_self, embSigma_eq_zero, embSigma_inj, embSigma_injective, embSigma_single, embSigma_zero, split_embSigma_of_ne, split_embSigma_self, support_embSigma	12
Total	13

Finsupp

Definitions

Name	Category	Theorems
embSigma 📖	CompOp	12 math math: embSigma_zero, embSigma_inj, embSigma_add, embSigma_eq_zero, embSigma_injective, split_embSigma_of_ne, support_embSigma, embSigma_apply_of_ne, embSigma_apply_self, embSigma_apply, embSigma_single, split_embSigma_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embSigma_add 📖	mathematical	—	embSigma AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Finsupp instAdd	—	ext embSigma_apply_self embSigma_apply_of_ne add_zero
embSigma_apply 📖	mathematical	—	DFunLike.coe Finsupp instFunLike embSigma	—	embDomain_apply_self sigma_mk_injective embDomain_notin_range Set.range_sigmaMk
embSigma_apply_of_ne 📖	mathematical	—	DFunLike.coe Finsupp instFunLike embSigma	—	embDomain_notin_range
embSigma_apply_self 📖	mathematical	—	DFunLike.coe Finsupp instFunLike embSigma	—	embSigma.eq_1 embDomain_apply_self
embSigma_eq_zero 📖	mathematical	—	embSigma Finsupp instZero	—	—
embSigma_inj 📖	mathematical	—	embSigma	—	embSigma_injective
embSigma_injective 📖	mathematical	—	Finsupp embSigma	—	ext embSigma_apply_self
embSigma_single 📖	mathematical	—	embSigma single	—	—
embSigma_zero 📖	mathematical	—	embSigma Finsupp instZero	—	—
split_embSigma_of_ne 📖	mathematical	—	split embSigma Finsupp instZero	—	ext split_apply embSigma_apply_of_ne
split_embSigma_self 📖	mathematical	—	split embSigma	—	ext split_apply embSigma_apply_self
support_embSigma 📖	mathematical	—	support embSigma Finset.map Function.Embedding.sigmaMk	—	—

---

← Back to Index