Commit 2025-11-24 11:02 d2adcc71

View on Github →

feat: Finsupp.embSigma {k : κ} (f : ι k →₀ M) : (Σ k, ι k) →₀ M (#31923) This is just embDomain (Embedding.sigmaMk k) f, and the basic lemmas describing it. I'm using this while exploring a potential definition of ConvexSpace. Mostly written by Claude, see commit history.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finsupp/Sigma.lean

added def Finsupp.embSigma

added theorem Finsupp.embSigma_add

added theorem Finsupp.embSigma_apply

added theorem Finsupp.embSigma_apply_of_ne

added theorem Finsupp.embSigma_apply_self

added theorem Finsupp.embSigma_eq_zero

added theorem Finsupp.embSigma_inj

added theorem Finsupp.embSigma_injective

added theorem Finsupp.embSigma_single

added theorem Finsupp.embSigma_zero

added theorem Finsupp.split_embSigma_of_ne

added theorem Finsupp.split_embSigma_self

added theorem Finsupp.support_embSigma