Theorems · Definition · general algebraic systems

Finsupp.splitComp

{ι : Type u_4} →
  {M : Type u_5} →
    {N : Type u_6} →
      {αs : ι → Type u_12} →
        [inst : Zero M] →
          ((i : ι) × αs i →₀ M) →
            [inst_1 : Zero N] →
              (g : (i : ι) → (αs i →₀ M) → N) → (∀ (i : ι) (x : αs i →₀ M), x = 0 ↔ g i x = 0) → ι →₀ N

Given l, a finitely supported function from the sigma type Σ i, αs i to β and an ι-indexed family g of functions from (αs i →₀ β) to γ, split_comp defines a finitely supported function from the index type ι to γ given by composing g i with split l i.

Defined in

Mathlib.Data.Finsupp.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

ZeroZero