Theorems · Definition · general algebraic systems

sigmaFinsuppLequivDFinsupp

{ι : Type u_1} →
  (R : Type u_2) →
    {η : ι → Type u_4} →
      {N : Type u_5} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid N] → [inst_2 : Module R N] → ((i : ι) × η i →₀ N) ≃ₗ[R] Π₀ (i : ι), η i →₀ N

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

Defined in

Mathlib.Data.Finsupp.ToDFinsupp

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModule