Theorems · Definition · linear algebra

MultilinearMap.mkPiRing

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

The canonical multilinear map on R^ι when ι is finite, associating to m the product of all the m i (multiplied by a fixed reference element z in the target module). See also mkPiAlgebra for a more general version.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleFintype