Theorems · Definition · linear algebra

MultilinearMap.freeFinsuppEquiv

{ι : Type u_1} →
  {ι' : Type u_2} →
    {R : Type u_3} →
      {κ : ι → Type u_4} →
        [DecidableEq ι] →
          [Fintype ι] →
            [inst : CommSemiring R] →
              [DecidableEq R] →
                [DecidableEq ι'] →
                  [(i : ι) → Fintype (κ i)] →
                    [(i : ι) → DecidableEq (κ i)] →
                      (((i : ι) → κ i) × ι' →₀ R) ≃ₗ[R] MultilinearMap R (fun i => κ i →₀ R) (ι' →₀ 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 finitely supported maps from (Π i, κ i) × ι' into R. This is the Finsupp version of MultilinearMap.freeDFinsuppEquiv.

Defined in

Mathlib.LinearAlgebra.Multilinear.Finsupp

Cited by

4 results in Mathlib

Foundations

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

Assumes

DecidableEqFintypeCommSemiringDecidableEqDecidableEqFintypeDecidableEq