Theorems · Definition · general algebraic systems

sigmaFinsuppEquivDFinsupp

{ι : Type u_1} → {η : ι → Type u_4} → {N : Type u_5} → [inst : Zero N] → ((i : ι) × η i →₀ N) ≃ Π₀ (i : ι), η i →₀ N

Finsupp.split is an equivalence between (Σ i, η i) →₀ N and Π₀ i, (η i →₀ N).

Defined in

Mathlib.Data.Finsupp.ToDFinsupp

Cited by

8 results in Mathlib

Foundations

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

Assumes

Zero