Theorem Finsupp.embSigma_apply_of_ne

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_apply_of_neView on Github →