Theorems · Definition · commutative algebra

TensorProduct

(R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_7) →
      (N : Type u_8) →
        [inst_1 : AddCommMonoid M] → [inst_2 : AddCommMonoid N] → [Module R M] → [Module R N] → Type (max u_7 u_8)

The tensor product of two modules M and N over the same commutative semiring R. The localized notations are M ⊗ N and M ⊗[R] N, accessed by open scoped TensorProduct.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Defs

Cited by

2,545 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidAddCommMonoidModuleModule