Theorems · Theorem · ring theory

Algebra.TensorProduct.mapOfCompatibleSMul_tmul

∀ (R : Type u_3) (S : Type u_4) (T : Type u_5) (A : Type u_6) (B : Type u_7) [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : Algebra S B] [inst_9 : Algebra T A]
  [inst_10 : SMulCommClass R T A] [inst_11 : SMulCommClass S T A] [inst_12 : SMulCommClass R S A]
  [inst_13 : TensorProduct.CompatibleSMul R S A B] (m : A) (n : B),
  (Algebra.TensorProduct.mapOfCompatibleSMul R S T A B) (m ⊗ₜ[S] n) = m ⊗ₜ[R] n

Defined in

Mathlib.RingTheory.TensorProduct.Maps

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringSemiringSemiringAlgebraAlgebraAlgebraAlgebraAlgebraSMulCommClassSMulCommClassSMulCommClassTensorProduct.CompatibleSMul