Theorems · Theorem · linear algebra

TensorProduct.prodRight_tmul

∀ (R : Type u_1) (S : Type u_2) (M₁ : Type u_3) (M₂ : Type u_4) (M₃ : Type u_5) [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid M₃]
  [inst_5 : Algebra R S] [inst_6 : Module R M₁] [inst_7 : Module S M₁] [inst_8 : IsScalarTower R S M₁]
  [inst_9 : Module R M₂] [inst_10 : Module R M₃] (m₁ : M₁) (m : M₂ × M₃),
  (TensorProduct.prodRight R S M₁ M₂ M₃) (m₁ ⊗ₜ[R] m) = (m₁ ⊗ₜ[R] m.1, m₁ ⊗ₜ[R] m.2)

Defined in

Mathlib.LinearAlgebra.TensorProduct.Prod

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAddCommMonoidAddCommMonoidAddCommMonoidAlgebraModuleModuleIsScalarTowerModuleModule