Theorems · Definition · linear algebra

TensorProduct.rid

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

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

Defined in

Mathlib.LinearAlgebra.TensorProduct.Associator

Cited by

63 results in Mathlib

Foundations

Depth 63 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModule