Theorems · Definition · linear algebra

MultilinearMap.piRingEquiv

{R : Type uR} →
  {ι : Type uι} →
    {M₂ : Type v₂} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₂] → [inst_2 : Module R M₂] → [Fintype ι] → M₂ ≃ₗ[R] MultilinearMap R (fun x => R) M₂

When ι is finite, multilinear maps on R^ι with values in M₂ are in bijection with M₂, as such a multilinear map is completely determined by its value on the constant vector made of ones. We register this bijection as a linear equivalence in MultilinearMap.piRingEquiv.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleFintype