Theorem Finsupp.support_embSigma

Modification history

2025-11-24 11:02
Mathlib/Data/Finsupp/Sigma.lean
feat: `Finsupp.embSigma {k : κ} (f : ι k →₀ M) : (Σ k, ι k) →₀ M` (#31923) …
Added Finsupp.support_embSigmaView on Github →