Theorems · Theorem · linear algebra

TensorProduct.lidOfCompatibleSMul_tmul

∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_4) (M : Type u_5) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : CommSemiring A] [inst_4 : Module A M] [inst_5 : Module R A] [inst_6 : SMulCommClass R A A]
  [inst_7 : TensorProduct.CompatibleSMul R A A M] [inst_8 : TensorProduct.CompatibleSMul A R A M] (a : A) (m : M),
  (TensorProduct.lidOfCompatibleSMul R A M) (a ⊗ₜ[R] m) = a • m

Defined in

Mathlib.LinearAlgebra.TensorProduct.Associator

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringAddCommMonoidModuleCommSemiringModuleModuleSMulCommClassTensorProduct.CompatibleSMulTensorProduct.CompatibleSMul