Theorems · Definition · linear algebra

MultilinearMap.ofSubsingleton

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

Equivalence between linear maps M₂ →ₗ[R] M₃ and one-multilinear maps.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

6 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Quot.sound

Assumes

SemiringAddCommMonoidAddCommMonoidModuleModuleSubsingleton