Theorems · Inductive type · ring theory

LinearMap.CompatibleSMul

(M : Type u_8) →
  (M₂ : Type u_10) →
    [inst : AddCommMonoid M] →
      [inst_1 : AddCommMonoid M₂] →
        (R : Type u_14) →
          (S : Type u_15) → [inst_2 : Semiring S] → [SMul R M] → [Module S M] → [SMul R M₂] → [Module S M₂] → Prop

A typeclass for SMul structures which can be moved through a LinearMap. 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 S does not support negation.

Defined in

Mathlib.Algebra.Module.LinearMap.Defs

Cited by

86 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

AddCommMonoidAddCommMonoidSemiringSMulModuleSMulModule