Documentation

Mathlib.Algebra.Module.LinearMap.Basic

(Semi)linear maps #

In this file we define

We then provide LinearMap with the following instances:

Implementation notes #

To ensure that composition works smoothly for semilinear maps, we use the typeclasses RingHomCompTriple, RingHomInvPair and RingHomSurjective from Mathlib.Algebra.Ring.CompTypeclasses.

Notation #

TODO #

Tags #

linear map

structure IsLinearMap (R : Type u) {M : Type v} {M₂ : Type w} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : MM₂) :

A map f between modules over a semiring is linear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = c • f x. The predicate IsLinearMap R f asserts this property. A bundled version is available with LinearMap, and should be favored over IsLinearMap most of the time.

  • map_add : ∀ (x y : M), f (x + y) = f x + f y

    A linear map preserves addition.

  • map_smul : ∀ (c : R) (x : M), f (c x) = c f x

    A linear map preserves scalar multiplication.

Instances For
    structure LinearMap {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_19) (M₂ : Type u_20) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends AddHom :
    Type (max u_19 u_20)

    A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x. Elements of LinearMap σ M M₂ (available under the notation M →ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which σ = RingHom.id R), the notation M →ₗ[R] M₂ is available. An unbundled version of plain linear maps is available with the predicate IsLinearMap, but it should be avoided most of the time.

    • toFun : MM₂
    • map_add' : ∀ (x y : M), self.toFun (x + y) = self.toFun x + self.toFun y
    • map_smul' : ∀ (m : R) (x : M), self.toFun (m x) = σ m self.toFun x

      The proposition that the function commutes with the actions.

    Instances For
      @[reducible]
      abbrev LinearMap.toMulActionHom {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] {σ : R →+* S} {M : Type u_19} {M₂ : Type u_20} [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] (self : M →ₛₗ[σ] M₂) :
      M →ₑ[σ] M₂

      The MulActionHom underlying a LinearMap.

      Equations
      Instances For

        M →ₛₗ[σ] N is the type of σ-semilinear maps from M to N.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          M →ₗ[R] N is the type of R-linear maps from M to N.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            M →ₗ⋆[R] N is the type of R-conjugate-linear maps from M to N.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              class SemilinearMapClass (F : Type u_17) {R : outParam (Type u_18)} {S : outParam (Type u_19)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_20)) (M₂ : outParam (Type u_21)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] [FunLike F M M₂] extends AddHomClass , MulActionSemiHomClass :

              SemilinearMapClass F σ M M₂ asserts F is a type of bundled σ-semilinear maps M → M₂.

              See also LinearMapClass F R M M₂ for the case where σ is the identity map on R.

              A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S is semilinear if it satisfies the two properties f (x + y) = f x + f y and f (c • x) = (σ c) • f x.

                Instances
                  @[inline, reducible]
                  abbrev LinearMapClass (F : Type u_17) (R : outParam (Type u_18)) (M : Type u_19) (M₂ : Type u_20) [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂] :

                  LinearMapClass F R M M₂ asserts F is a type of bundled R-linear maps M → M₂.

                  This is an abbreviation for SemilinearMapClass F (RingHom.id R) M M₂.

                  Equations
                  Instances For
                    @[simp]
                    theorem LinearMapClass.map_smul {R : outParam (Type u_17)} {M : outParam (Type u_18)} {M₂ : outParam (Type u_19)} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {F : Type u_20} [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) :
                    f (r x) = r f x
                    instance SemilinearMapClass.instAddMonoidHomClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} (F : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
                    Equations
                    • =
                    instance SemilinearMapClass.distribMulActionSemiHomClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} (F : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
                    Equations
                    • =
                    theorem SemilinearMapClass.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : F) [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
                    c f x = f (σ' c x)
                    def SemilinearMapClass.semilinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : F) [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
                    M →ₛₗ[σ] M₃

                    Reinterpret an element of a type of semilinear maps as a semilinear map.

                    Equations
                    • f = { toAddHom := { toFun := f, map_add' := }, map_smul' := }
                    Instances For
                      instance SemilinearMapClass.instCoeToSemilinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} {F : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
                      CoeHead F (M →ₛₗ[σ] M₃)

                      Reinterpret an element of a type of semilinear maps as a semilinear map.

                      Equations
                      • SemilinearMapClass.instCoeToSemilinearMap = { coe := fun (f : F) => f }
                      @[inline, reducible]
                      abbrev LinearMapClass.linearMap {R : Type u_1} {M₁ : Type u_10} {M₂ : Type u_11} {F : Type u_17} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (f : F) [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] :
                      M₁ →ₗ[R] M₂

                      Reinterpret an element of a type of linear maps as a linear map.

                      Equations
                      Instances For
                        instance LinearMapClass.instCoeToLinearMap {R : Type u_1} {M₁ : Type u_10} {M₂ : Type u_11} {F : Type u_17} [Semiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] [FunLike F M₁ M₂] [LinearMapClass F R M₁ M₂] :
                        CoeHead F (M₁ →ₗ[R] M₂)

                        Reinterpret an element of a type of linear maps as a linear map.

                        Equations
                        • LinearMapClass.instCoeToLinearMap = { coe := fun (f : F) => f }
                        instance LinearMap.instFunLike {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                        FunLike (M →ₛₗ[σ] M₃) M M₃
                        Equations
                        • LinearMap.instFunLike = { coe := fun (f : M →ₛₗ[σ] M₃) => f.toFun, coe_injective' := }
                        instance LinearMap.semilinearMapClass {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                        SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
                        Equations
                        • =
                        def LinearMap.toDistribMulActionHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
                        M →ₑ+[σ] M₃

                        The DistribMulActionHom underlying a LinearMap.

                        Equations
                        Instances For
                          @[simp]
                          theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
                          f.toAddHom = f
                          theorem LinearMap.toFun_eq_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} :
                          f.toFun = f
                          theorem LinearMap.ext {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : ∀ (x : M), f x = g x) :
                          f = g
                          def LinearMap.copy {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
                          M →ₛₗ[σ] M₃

                          Copy of a LinearMap with a new toFun equal to the old one. Useful to fix definitional equalities.

                          Equations
                          • LinearMap.copy f f' h = { toAddHom := { toFun := f', map_add' := }, map_smul' := }
                          Instances For
                            @[simp]
                            theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
                            (LinearMap.copy f f' h) = f'
                            theorem LinearMap.copy_eq {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
                            LinearMap.copy f f' h = f
                            @[simp]
                            theorem LinearMap.coe_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (m : R) (x : M), f.toFun (m x) = σ m f.toFun x) :
                            { toAddHom := f, map_smul' := h } = f
                            @[simp]
                            theorem LinearMap.coe_addHom_mk {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (m : R) (x : M), f.toFun (m x) = σ m f.toFun x) :
                            { toAddHom := f, map_smul' := h } = f
                            theorem LinearMap.coe_semilinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_17} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
                            f = f
                            theorem LinearMap.toLinearMap_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_17} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} {g : F} (h : f = g) :
                            f = g
                            def LinearMap.id {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] :

                            Identity map as a LinearMap

                            Equations
                            • LinearMap.id = let __src := DistribMulActionHom.id R; { toAddHom := { toFun := id, map_add' := }, map_smul' := }
                            Instances For
                              theorem LinearMap.id_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
                              LinearMap.id x = x
                              @[simp]
                              theorem LinearMap.id_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] :
                              LinearMap.id = id
                              @[simp]
                              theorem LinearMap.id'_apply {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] (x : M) :
                              LinearMap.id' x = x
                              def LinearMap.id' {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] :

                              A generalisation of LinearMap.id that constructs the identity function as a σ-semilinear map for any ring homomorphism σ which we know is the identity.

                              Equations
                              • LinearMap.id' = { toAddHom := { toFun := fun (x : M) => x, map_add' := }, map_smul' := }
                              Instances For
                                @[simp]
                                theorem LinearMap.id'_coe {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] :
                                LinearMap.id' = id
                                theorem LinearMap.isLinear {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) :
                                IsLinearMap R fₗ
                                theorem LinearMap.coe_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                                Function.Injective DFunLike.coe
                                theorem LinearMap.congr_arg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {x : M} {x' : M} :
                                x = x'f x = f x'
                                theorem LinearMap.congr_fun {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} (h : f = g) (x : M) :
                                f x = g x

                                If two linear maps are equal, they are equal at each point.

                                theorem LinearMap.ext_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {g : M →ₛₗ[σ] M₃} :
                                f = g ∀ (x : M), f x = g x
                                @[simp]
                                theorem LinearMap.mk_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ∀ (m : R) (x : M), (f).toFun (m x) = σ m (f).toFun x) :
                                { toAddHom := f, map_smul' := h } = f
                                theorem LinearMap.map_add {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (x : M) (y : M) :
                                f (x + y) = f x + f y
                                theorem LinearMap.map_zero {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
                                f 0 = 0
                                @[simp]
                                theorem LinearMap.map_smulₛₗ {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (c : R) (x : M) :
                                f (c x) = σ c f x
                                theorem LinearMap.map_smul {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (fₗ : M →ₗ[R] M₂) (c : R) (x : M) :
                                fₗ (c x) = c fₗ x
                                theorem LinearMap.map_smul_inv {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [RingHomInvPair σ σ'] (c : S) (x : M) :
                                c f x = f (σ' c x)
                                @[simp]
                                theorem LinearMap.map_eq_zero_iff {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : Function.Injective f) {x : M} :
                                f x = 0 x = 0
                                class LinearMap.CompatibleSMul (M : Type u_9) (M₂ : Type u_11) [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_17) (S : Type u_18) [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] :

                                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.intModule, allowing z • to be moved even if R does not support negation.

                                • map_smul : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c x) = c fₗ x

                                  Scalar multiplication by R of M can be moved through linear maps.

                                Instances
                                  instance LinearMap.IsScalarTower.compatibleSMul {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [IsScalarTower R S M] [IsScalarTower R S M₂] :
                                  Equations
                                  • =
                                  instance LinearMap.IsScalarTower.compatibleSMul' {M : Type u_9} [AddCommMonoid M] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R S] [IsScalarTower R S M] :
                                  Equations
                                  • =
                                  @[simp]
                                  theorem LinearMap.map_smul_of_tower {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_17} {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
                                  fₗ (c x) = c fₗ x
                                  theorem LinearMap.isScalarTower_of_injective {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_17) {S : Type u_18} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [LinearMap.CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective f) :
                                  theorem LinearMap.isLinearMap_of_compatibleSMul (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
                                  def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
                                  M →+ M₃

                                  convert a linear map to an additive map

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem LinearMap.toAddMonoidHom_coe {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
                                    def LinearMap.restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) :
                                    M →ₗ[R] M₂

                                    If M and M₂ are both R-modules and S-modules and R-module structures are defined by an action of R on S (formally, we have two scalar towers), then any S-linear map from M to M₂ is R-linear.

                                    See also LinearMap.map_smul_of_tower.

                                    Equations
                                    • R fₗ = { toAddHom := { toFun := fₗ, map_add' := }, map_smul' := }
                                    Instances For
                                      instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :
                                      CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)
                                      Equations
                                      @[simp]
                                      theorem LinearMap.coe_restrictScalars (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
                                      (R f) = f
                                      theorem LinearMap.restrictScalars_apply (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M) :
                                      (R fₗ) x = fₗ x
                                      theorem LinearMap.restrictScalars_injective (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :
                                      @[simp]
                                      theorem LinearMap.restrictScalars_inj (R : Type u_1) {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (gₗ : M →ₗ[S] M₂) :
                                      R fₗ = R gₗ fₗ = gₗ
                                      theorem LinearMap.toAddMonoidHom_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                                      Function.Injective LinearMap.toAddMonoidHom
                                      theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : R →+* S} {f : R →ₛₗ[σ] M₃} {g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) :
                                      f = g

                                      If two σ-linear maps from R are equal on 1, then they are equal.

                                      theorem LinearMap.ext_ring_iff {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} {f : R →ₛₗ[σ] M} {g : R →ₛₗ[σ] M} :
                                      f = g f 1 = g 1
                                      theorem LinearMap.ext_ring_op {R : Type u_1} {S : Type u_6} {M₃ : Type u_12} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : Rᵐᵒᵖ →+* S} {f : R →ₛₗ[σ] M₃} {g : R →ₛₗ[σ] M₃} (h : f 1 = g 1) :
                                      f = g
                                      @[simp]
                                      theorem RingHom.toSemilinearMap_apply {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R →+* S) :
                                      ∀ (a : R), (RingHom.toSemilinearMap f) a = f.toFun a
                                      def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_6} [Semiring R] [Semiring S] (f : R →+* S) :

                                      Interpret a RingHom f as an f-semilinear map.

                                      Equations
                                      Instances For
                                        def LinearMap.comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
                                        M₁ →ₛₗ[σ₁₃] M₃

                                        Composition of two linear maps is a linear map

                                        Equations
                                        • LinearMap.comp f g = { toAddHom := { toFun := f g, map_add' := }, map_smul' := }
                                        Instances For

                                          ∘ₗ is notation for composition of two linear (not semilinear!) maps into a linear map. This is useful when Lean is struggling to infer the RingHomCompTriple instance.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For

                                            Pretty printer defined by notation3 command.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              theorem LinearMap.comp_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) (x : M₁) :
                                              (LinearMap.comp f g) x = f (g x)
                                              @[simp]
                                              theorem LinearMap.coe_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
                                              (LinearMap.comp f g) = f g
                                              @[simp]
                                              theorem LinearMap.comp_id {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
                                              LinearMap.comp f LinearMap.id = f
                                              @[simp]
                                              theorem LinearMap.id_comp {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
                                              LinearMap.comp LinearMap.id f = f
                                              theorem LinearMap.comp_assoc {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {R₄ : Type u_17} {M₄ : Type u_18} [Semiring R₄] [AddCommMonoid M₄] [Module R₄ M₄] {σ₃₄ : R₃ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (f : M₁ →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₃ →ₛₗ[σ₃₄] M₄) :
                                              theorem Function.Surjective.injective_linearMapComp_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {g : M₁ →ₛₗ[σ₁₂] M₂} (hg : Function.Surjective g) :
                                              Function.Injective fun (f : M₂ →ₛₗ[σ₂₃] M₃) => LinearMap.comp f g

                                              The linear map version of Function.Surjective.injective_comp_right

                                              @[simp]
                                              theorem LinearMap.cancel_right {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃} (hg : Function.Surjective g) :
                                              theorem Function.Injective.injective_linearMapComp_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} (hf : Function.Injective f) :
                                              Function.Injective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => LinearMap.comp f g

                                              The linear map version of Function.Injective.comp_left

                                              @[simp]
                                              theorem LinearMap.cancel_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_10} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : Function.Injective f) :
                                              def LinearMap.inverse {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] (f : M →ₛₗ[σ] M₂) (g : M₂M) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
                                              M₂ →ₛₗ[σ'] M

                                              If a function g is a left and right inverse of a linear map f, then g is linear itself.

                                              Equations
                                              • LinearMap.inverse f g h₁ h₂ = { toAddHom := { toFun := g, map_add' := }, map_smul' := }
                                              Instances For
                                                theorem LinearMap.map_neg {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) :
                                                f (-x) = -f x
                                                theorem LinearMap.map_sub {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x : M) (y : M) :
                                                f (x - y) = f x - f y
                                                instance LinearMap.CompatibleSMul.intModule {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] {S : Type u_17} [Semiring S] [Module S M] [Module S M₂] :
                                                Equations
                                                • =
                                                instance LinearMap.CompatibleSMul.units {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_17} {S : Type u_18} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂] [LinearMap.CompatibleSMul M M₂ R S] :
                                                Equations
                                                • =
                                                @[simp]
                                                theorem Module.compHom.toLinearMap_apply {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R →+* S) (a : R) :
                                                def Module.compHom.toLinearMap {R : Type u_17} {S : Type u_18} [Semiring R] [Semiring S] (g : R →+* S) :

                                                g : R →+* S is R-linear when the module structure on S is Module.compHom S g .

                                                Equations
                                                Instances For
                                                  def DistribMulActionHom.toSemilinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} (fₗ : M →ₑ+[σ] M₂) :
                                                  M →ₛₗ[σ] M₂

                                                  A DistribMulActionHom between two modules is a linear map.

                                                  Equations
                                                  • fₗ = { toAddHom := { toFun := fₗ.toFun, map_add' := }, map_smul' := }
                                                  Instances For
                                                    def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_9} {M₃ : Type u_12} [AddCommMonoid M] [AddCommMonoid M₃] [Semiring R] [Module R M] [Module R M₃] (fₗ : M →+[R] M₃) :
                                                    M →ₗ[R] M₃

                                                    A DistribMulActionHom between two modules is a linear map.

                                                    Equations
                                                    Instances For
                                                      instance DistribMulActionHom.instCoeTCLinearMap {R : Type u_1} {M : Type u_9} {M₃ : Type u_12} [AddCommMonoid M] [AddCommMonoid M₃] [Semiring R] [Module R M] [Module R M₃] :
                                                      CoeTC (M →+[R] M₃) (M →ₗ[R] M₃)
                                                      Equations
                                                      • DistribMulActionHom.instCoeTCLinearMap = { coe := DistribMulActionHom.toLinearMap }
                                                      @[simp]
                                                      theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} (f : M →ₑ+[σ] M₂) :
                                                      f = f
                                                      theorem DistribMulActionHom.toLinearMap_injective {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} {f : M →ₑ+[σ] M₂} {g : M →ₑ+[σ] M₂} (h : f = g) :
                                                      f = g
                                                      def IsLinearMap.mk' {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : MM₂) (H : IsLinearMap R f) :
                                                      M →ₗ[R] M₂

                                                      Convert an IsLinearMap predicate to a LinearMap

                                                      Equations
                                                      • IsLinearMap.mk' f H = { toAddHom := { toFun := f, map_add' := }, map_smul' := }
                                                      Instances For
                                                        @[simp]
                                                        theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : MM₂} (H : IsLinearMap R f) (x : M) :
                                                        (IsLinearMap.mk' f H) x = f x
                                                        theorem IsLinearMap.isLinearMap_smul {R : Type u_17} {M : Type u_18} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) :
                                                        IsLinearMap R fun (z : M) => c z
                                                        theorem IsLinearMap.isLinearMap_smul' {R : Type u_17} {M : Type u_18} [Semiring R] [AddCommMonoid M] [Module R M] (a : M) :
                                                        IsLinearMap R fun (c : R) => c a
                                                        theorem IsLinearMap.map_zero {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : MM₂} (lin : IsLinearMap R f) :
                                                        f 0 = 0
                                                        theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_9} [Semiring R] [AddCommGroup M] [Module R M] :
                                                        IsLinearMap R fun (z : M) => -z
                                                        theorem IsLinearMap.map_neg {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : MM₂} (lin : IsLinearMap R f) (x : M) :
                                                        f (-x) = -f x
                                                        theorem IsLinearMap.map_sub {R : Type u_1} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : MM₂} (lin : IsLinearMap R f) (x : M) (y : M) :
                                                        f (x - y) = f x - f y
                                                        def AddMonoidHom.toNatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) :

                                                        Reinterpret an additive homomorphism as an -linear map.

                                                        Equations
                                                        Instances For
                                                          theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₂] :
                                                          Function.Injective AddMonoidHom.toNatLinearMap
                                                          def AddMonoidHom.toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :

                                                          Reinterpret an additive homomorphism as a -linear map.

                                                          Equations
                                                          Instances For
                                                            theorem AddMonoidHom.toIntLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] :
                                                            Function.Injective AddMonoidHom.toIntLinearMap
                                                            @[simp]
                                                            theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
                                                            def AddMonoidHom.toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module M] [AddCommGroup M₂] [Module M₂] (f : M →+ M₂) :

                                                            Reinterpret an additive homomorphism as a -linear map.

                                                            Equations
                                                            Instances For
                                                              theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module M] [AddCommGroup M₂] [Module M₂] :
                                                              Function.Injective AddMonoidHom.toRatLinearMap
                                                              @[simp]
                                                              theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_9} {M₂ : Type u_11} [AddCommGroup M] [Module M] [AddCommGroup M₂] [Module M₂] (f : M →+ M₂) :
                                                              instance LinearMap.instSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] :
                                                              SMul S (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • LinearMap.instSMulLinearMap = { smul := fun (a : S) (f : M →ₛₗ[σ₁₂] M₂) => { toAddHom := { toFun := a f, map_add' := }, map_smul' := } }
                                                              @[simp]
                                                              theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
                                                              (a f) x = a f x
                                                              theorem LinearMap.coe_smul {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) :
                                                              (a f) = a f
                                                              instance LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {T : Type u_8} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMulCommClass S T M₂] :
                                                              SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • =
                                                              instance LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {T : Type u_8} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [Monoid T] [DistribMulAction T M₂] [SMulCommClass R₂ T M₂] [SMul S T] [IsScalarTower S T M₂] :
                                                              IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • =
                                                              instance LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeInstMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] [DistribMulAction Sᵐᵒᵖ M₂] [SMulCommClass R₂ Sᵐᵒᵖ M₂] [IsCentralScalar S M₂] :
                                                              IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • =
                                                              instance LinearMap.instSMulDomMulActLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :
                                                              SMul S'ᵈᵐᵃ (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • LinearMap.instSMulDomMulActLinearMap = { smul := fun (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) => { toAddHom := { toFun := a f, map_add' := }, map_smul' := } }
                                                              theorem DomMulAct.smul_linearMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
                                                              (a f) x = f (DomMulAct.mk.symm a x)
                                                              @[simp]
                                                              theorem DomMulAct.mk_smul_linearMap_apply {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S') (f : M →ₛₗ[σ₁₂] M₂) (x : M) :
                                                              (DomMulAct.mk a f) x = f (a x)
                                                              theorem DomMulAct.coe_smul_linearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] (a : S'ᵈᵐᵃ) (f : M →ₛₗ[σ₁₂] M₂) :
                                                              (a f) = a f
                                                              instance LinearMap.instSMulCommClassDomMulActDomMulActLinearMapInstSMulDomMulActLinearMapInstSMulDomMulActLinearMap {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} {T' : Type u_18} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] [Monoid T'] [DistribMulAction T' M] [SMulCommClass R T' M] [SMulCommClass S' T' M] :
                                                              Equations
                                                              • =

                                                              Arithmetic on the codomain #

                                                              instance LinearMap.instZeroLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                              Zero (M →ₛₗ[σ₁₂] M₂)

                                                              The constant 0 map is linear.

                                                              Equations
                                                              • LinearMap.instZeroLinearMap = { zero := { toAddHom := { toFun := 0, map_add' := }, map_smul' := } }
                                                              @[simp]
                                                              theorem LinearMap.zero_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (x : M) :
                                                              0 x = 0
                                                              @[simp]
                                                              theorem LinearMap.comp_zero {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) :
                                                              @[simp]
                                                              theorem LinearMap.zero_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) :
                                                              instance LinearMap.instInhabitedLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                              Inhabited (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • LinearMap.instInhabitedLinearMap = { default := 0 }
                                                              @[simp]
                                                              theorem LinearMap.default_def {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                              default = 0
                                                              instance LinearMap.instAddLinearMap {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                              Add (M →ₛₗ[σ₁₂] M₂)

                                                              The sum of two linear maps is linear.

                                                              Equations
                                                              • LinearMap.instAddLinearMap = { add := fun (f g : M →ₛₗ[σ₁₂] M₂) => { toAddHom := { toFun := f + g, map_add' := }, map_smul' := } }
                                                              @[simp]
                                                              theorem LinearMap.add_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (x : M) :
                                                              (f + g) x = f x + g x
                                                              theorem LinearMap.add_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₂ →ₛₗ[σ₂₃] M₃) :
                                                              theorem LinearMap.comp_add {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
                                                              instance LinearMap.addCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                              AddCommMonoid (M →ₛₗ[σ₁₂] M₂)

                                                              The type of linear maps is an additive monoid.

                                                              Equations
                                                              instance LinearMap.instNegLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
                                                              Neg (M →ₛₗ[σ₁₂] N₂)

                                                              The negation of a linear map is linear.

                                                              Equations
                                                              • LinearMap.instNegLinearMapToAddCommMonoid = { neg := fun (f : M →ₛₗ[σ₁₂] N₂) => { toAddHom := { toFun := -f, map_add' := }, map_smul' := } }
                                                              @[simp]
                                                              theorem LinearMap.neg_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (x : M) :
                                                              (-f) x = -f x
                                                              @[simp]
                                                              theorem LinearMap.neg_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) :
                                                              @[simp]
                                                              theorem LinearMap.comp_neg {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {N₂ : Type u_14} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) :
                                                              instance LinearMap.instSubLinearMapToAddCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
                                                              Sub (M →ₛₗ[σ₁₂] N₂)

                                                              The subtraction of two linear maps is linear.

                                                              Equations
                                                              • LinearMap.instSubLinearMapToAddCommMonoid = { sub := fun (f g : M →ₛₗ[σ₁₂] N₂) => { toAddHom := { toFun := f - g, map_add' := }, map_smul' := } }
                                                              @[simp]
                                                              theorem LinearMap.sub_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (x : M) :
                                                              (f - g) x = f x - g x
                                                              theorem LinearMap.sub_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {M₂ : Type u_11} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ M₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) (h : M₂ →ₛₗ[σ₂₃] N₃) :
                                                              theorem LinearMap.comp_sub {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_9} {N₂ : Type u_14} {N₃ : Type u_15} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommGroup N₂] [AddCommGroup N₃] [Module R₁ M] [Module R₂ N₂] [Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
                                                              instance LinearMap.addCommGroup {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_9} {N₂ : Type u_14} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
                                                              AddCommGroup (M →ₛₗ[σ₁₂] N₂)

                                                              The type of linear maps is an additive group.

                                                              Equations
                                                              instance LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Monoid S] [DistribMulAction S M₂] [SMulCommClass R₂ S M₂] :
                                                              DistribMulAction S (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              theorem LinearMap.smul_comp {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {S₃ : Type u_7} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R] [Semiring R₂] [Semiring R₃] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Module R₂ M₂] [Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [Monoid S₃] [DistribMulAction S₃ M₃] [SMulCommClass R₃ S₃ M₃] (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) :
                                                              theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} {M₃ : Type u_12} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [AddCommMonoid M₃] [Module R M] [Monoid S] [DistribMulAction S M₂] [Module R M₂] [Module R M₃] [SMulCommClass R S M₂] [DistribMulAction S M₃] [SMulCommClass R S M₃] [LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
                                                              g ∘ₗ (a f) = a g ∘ₗ f
                                                              instance LinearMap.instDistribMulActionDomMulActLinearMapInstMonoidDomMulActInstMonoidToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_3} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} {S' : Type u_17} [Monoid S'] [DistribMulAction S' M] [SMulCommClass R S' M] :
                                                              Equations
                                                              • LinearMap.instDistribMulActionDomMulActLinearMapInstMonoidDomMulActInstMonoidToAddMonoidAddCommMonoid = DistribMulAction.mk
                                                              instance LinearMap.module {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] :
                                                              Module S (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              instance LinearMap.instNoZeroSMulDivisorsLinearMapToZeroToMonoidWithZeroInstZeroLinearMapInstSMulLinearMapToMonoidToDistribMulAction {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M₂] [SMulCommClass R₂ S M₂] [NoZeroSMulDivisors S M₂] :
                                                              NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • =
                                                              instance LinearMap.instModuleDomMulActLinearMapInstSemiringDomMulActInstSemiringAddCommMonoid {R : Type u_1} {R₂ : Type u_3} {S : Type u_6} {M : Type u_9} {M₂ : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {σ₁₂ : R →+* R₂} [Semiring S] [Module S M] [SMulCommClass R S M] :
                                                              Module Sᵈᵐᵃ (M →ₛₗ[σ₁₂] M₂)
                                                              Equations
                                                              • LinearMap.instModuleDomMulActLinearMapInstSemiringDomMulActInstSemiringAddCommMonoid = Module.mk