Theorems · Definition · general algebraic systems

Finsupp.embSigma

{κ : Type u_1} → {ι : κ → Type u_2} → {M : Type u_3} → [inst : Zero M] → {k : κ} → (ι k →₀ M) → (k : κ) × ι k →₀ M

Embed a finitely supported function f : ι k →₀ M into the k-th summand of the sigma type (Σ k, ι k) →₀ M. This is Finsupp.embDomain specialized to Function.Embedding.sigmaMk k.

Defined in

Mathlib.Data.Finsupp.Sigma

Cited by

12 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Zero