Theorems · Theorem · commutative algebra

TensorProduct.CompatibleSMul.smul_tmul

∀ {R : Type u_1} {R' : Type u_4} {inst : CommSemiring R} {inst_1 : Monoid R'} {M : Type u_7} {N : Type u_8}
  {inst_2 : AddCommMonoid M} {inst_3 : AddCommMonoid N} {inst_4 : DistribMulAction R' M} {inst_5 : Module R M}
  {inst_6 : Module R N} {inst_7 : DistribMulAction R' N} [self : TensorProduct.CompatibleSMul R R' M N] (r : R') (m : M)
  (n : N), (r • m) ⊗ₜ[R] n = m ⊗ₜ[R] (r • n)

Defined in

Mathlib.LinearAlgebra.TensorProduct.Defs

Cited by

2 results in Mathlib

Foundations

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

Assumes

TensorProduct.CompatibleSMul