Theorems · Definition · linear algebra

PiTensorProduct

{ι : Type u_1} →
  (R : Type u_4) →
    [inst : CommSemiring R] →
      (s : ι → Type u_7) →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] → [(i : ι) → Module R (s i)] → Type (max (max u_1 u_4) u_7)

PiTensorProduct R s with R a commutative semiring and s : ι → Type* is the tensor product of all the s i's. This is denoted by ⨂[R] i, s i.

Defined in

Mathlib.LinearAlgebra.PiTensorProduct.Basic

Cited by

181 results in Mathlib

Foundations

Depth 39 from the axioms, rests on 453 definitions · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule