Theorems · Definition · linear algebra

TensorPower.multilinearMapToDual

(R : Type u_1) →
  (M : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (n : ℕ) → MultilinearMap R (fun x => Module.Dual R M) (Module.Dual R (TensorPower R n M))

The canonical multilinear map from n copies of the dual of the module M to the dual of ⨂[R]^n M.

Defined in

Mathlib.LinearAlgebra.TensorPower.Pairing

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModule