Theorems · Definition · linear algebra

TensorProduct.lid

(R : Type u_1) →
  [inst : CommSemiring R] →
    (M : Type u_5) → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → TensorProduct R R M ≃ₗ[R] M

The base ring is a left identity for the tensor product of modules, up to linear equivalence.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Associator

Cited by

96 results in Mathlib

Foundations

Depth 60 from the axioms, rests on 940 definitions · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule