Theorem Finsupp.embSigma_single

Modification history

2025-11-26 22:53
Mathlib/Data/Finsupp/Sigma.lean
chore: fix more unused decidable instances in types (#32153) …
Modified Finsupp.embSigma_singleView on Github →
2025-11-24 11:02
Mathlib/Data/Finsupp/Sigma.lean
feat: `Finsupp.embSigma {k : κ} (f : ι k →₀ M) : (Σ k, ι k) →₀ M` (#31923) …
Added Finsupp.embSigma_singleView on Github →