Theorems · Inductive type · commutative algebra

TensorProduct.CompatibleSMul

(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] →
                [DistribMulAction R' M] → [Module R M] → [Module R N] → [DistribMulAction R' N] → Prop

A typeclass for SMul structures which can be moved across a tensor product. This typeclass is generated automatically from an IsScalarTower instance, but exists so that we can also add an instance for AddCommGroup.toIntModule, allowing z • to be moved even if R does not support negation. Note that Module R' (M ⊗[R] N) is available even without this typeclass on R'; it's only needed if TensorProduct.smul_tmul, TensorProduct.smul_tmul', or TensorProduct.tmul_smul is used.

Defined in

Mathlib.LinearAlgebra.TensorProduct.Defs

Cited by

17 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommSemiringMonoidAddCommMonoidAddCommMonoidDistribMulActionModuleModuleDistribMulAction