Theorem Finsupp.embSigma_inj

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.embSigma_injView on Github →