Theorems · Definition · commutative algebra

Algebra.TensorProduct.mul

{R : Type uR} →
  {A : Type uA} →
    {B : Type uB} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [SMulCommClass R A A] →
              [IsScalarTower R A A] →
                [inst_5 : NonUnitalNonAssocSemiring B] →
                  [inst_6 : Module R B] →
                    [SMulCommClass R B B] →
                      [IsScalarTower R B B] → TensorProduct R A B →ₗ[R] TensorProduct R A B →ₗ[R] TensorProduct R A B

(Implementation detail) The multiplication map on A ⊗[R] B, as an R-bilinear map.

Defined in

Mathlib.RingTheory.TensorProduct.Basic

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommSemiringNonUnitalNonAssocSemiringModuleSMulCommClassIsScalarTowerNonUnitalNonAssocSemiringModuleSMulCommClassIsScalarTower