Theorems · Definition · linear algebra

MultilinearMap.freeDFinsuppEquiv

{ι : Type uι} →
  {κ : ι → Type uκ} →
    {R : Type uR} →
      {ι' : Type u_1} →
        [DecidableEq ι] →
          [Fintype ι] →
            [inst : CommSemiring R] →
              [(i : ι) → Fintype (κ i)] →
                [(i : ι) → DecidableEq (κ i)] →
                  (Π₀ (x : ((i : ι) → κ i) × ι'), R) ≃ₗ[R] MultilinearMap R (fun i => Π₀ (x : κ i), R) (Π₀ (x : ι'), R)

The linear equivalence of multilinear maps on free modules over R indexed by fun i => κ i on the domain and ι' on the codomain and the dependent, finitely supported maps from (Π i, κ i) × ι' into R.

Defined in

Mathlib.LinearAlgebra.Multilinear.DFinsupp

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommSemiringFintypeDecidableEq