Theorems · Definition · linear algebra

MultilinearMap.mkPiAlgebra

(R : Type uR) →
  (ι : Type uι) →
    [inst : CommSemiring R] →
      (A : Type u_1) →
        [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → [Fintype ι] → MultilinearMap R (fun x => A) A

Given an R-algebra A, mkPiAlgebra is the multilinear map on A^ι associating to m the product of all the m i. See also MultilinearMap.mkPiAlgebraFin for a version that works with a non-commutative algebra A but requires ι = Fin n.

Defined in

Mathlib.LinearAlgebra.Multilinear.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraFintype