Documentation

Mathlib.Algebra.Module.LinearMap.Defs

(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.lean.

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_14} {S : Type u_15} [Semiring R] [Semiring S] (σ : R →+* S) (M : Type u_16) (M₂ : Type u_17) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₙ+ M₂, M →ₑ[σ] M₂ :
    Type (max u_16 u_17)

    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.

    Instances For

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

      Equations
        Instances For

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

          Equations
            Instances For
              class SemilinearMapClass (F : Type u_14) {R : outParam (Type u_15)} {S : outParam (Type u_16)} [Semiring R] [Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_17)) (M₂ : outParam (Type u_18)) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] [FunLike F M M₂] extends AddHomClass F M M₂, MulActionSemiHomClass F (⇑σ) M M₂ :

              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
                @[reducible, inline]
                abbrev LinearMapClass (F : Type u_14) (R : outParam (Type u_15)) (M : Type u_16) (M₂ : Type u_17) [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
                    theorem LinearMapClass.map_smul {R : outParam (Type u_14)} {M : outParam (Type u_15)} {M₂ : outParam (Type u_16)} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {F : Type u_17} [FunLike F M M₂] [LinearMapClass F R M M₂] (f : F) (r : R) (x : M) :
                    f (r x) = r f x
                    @[instance 100]
                    instance SemilinearMapClass.instAddMonoidHomClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} (F : Type u_14) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
                    @[instance 100]
                    instance SemilinearMapClass.distribMulActionSemiHomClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} (F : Type u_14) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] :
                    theorem SemilinearMapClass.map_smul_inv {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [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_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [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
                      Instances For
                        instance SemilinearMapClass.instCoeToSemilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} {F : Type u_14} [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
                          @[reducible, inline]
                          abbrev LinearMapClass.linearMap {R : Type u_1} {M₁ : Type u_9} {M₂ : Type u_10} {F : Type u_14} [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_9} {M₂ : Type u_10} {F : Type u_14} [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
                                instance LinearMap.instFunLike {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                                FunLike (M →ₛₗ[σ] M₃) M M₃
                                Equations
                                  instance LinearMap.semilinearMapClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                                  SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
                                  @[simp]
                                  theorem LinearMap.coe_coe {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_14} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f : F} :
                                  f = f
                                  def LinearMap.toDistribMulActionHom {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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_5} {M : Type u_8} {M₃ : Type u_11} [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_5} {M : Type u_8} {M₃ : Type u_11} [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_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f g : M →ₛₗ[σ] M₃} (h : ∀ (x : M), f x = g x) :
                                      f = g
                                      theorem LinearMap.ext_iff {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f g : M →ₛₗ[σ] M₃} :
                                      f = g ∀ (x : M), f x = g x
                                      def LinearMap.copy {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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
                                        Instances For
                                          @[simp]
                                          theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
                                          (f.copy f' h) = f'
                                          theorem LinearMap.copy_eq {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (f' : MM₃) (h : f' = f) :
                                          f.copy f' h = f
                                          @[simp]
                                          theorem LinearMap.coe_mk {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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
                                          @[simp]
                                          theorem LinearMap.coe_addHom_mk {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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.coe_semilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_14} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] (f : F) :
                                          f = f
                                          theorem LinearMap.toLinearMap_injective {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {F : Type u_14} [FunLike F M M₃] [SemilinearMapClass F σ M M₃] {f g : F} (h : f = g) :
                                          f = g
                                          def LinearMap.id {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :

                                          Identity map as a LinearMap

                                          Equations
                                            Instances For
                                              theorem LinearMap.id_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
                                              id x = x
                                              @[simp]
                                              theorem LinearMap.id_coe {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] :
                                              def LinearMap.id' {R : Type u_1} {M : Type u_8} [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
                                                Instances For
                                                  @[simp]
                                                  theorem LinearMap.id'_apply {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] (x : M) :
                                                  id' x = x
                                                  @[simp]
                                                  theorem LinearMap.id'_coe {R : Type u_1} {M : Type u_8} [Semiring R] [AddCommMonoid M] [Module R M] {σ : R →+* R} [RingHomId σ] :
                                                  theorem LinearMap.isLinear {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                                                  theorem LinearMap.congr_arg {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} {x x' : M} :
                                                  x = x'f x = f x'
                                                  theorem LinearMap.congr_fun {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} {f g : M →ₛₗ[σ] M₃} (h : f = g) (x : M) :
                                                  f x = g x

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

                                                  @[simp]
                                                  theorem LinearMap.mk_coe {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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
                                                  @[simp]
                                                  theorem LinearMap.mk_coe' {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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.toAddHom, map_smul' := h } = f
                                                  theorem LinearMap.map_add {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (x y : M) :
                                                  f (x + y) = f x + f y
                                                  theorem LinearMap.map_zero {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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_5} {M : Type u_8} {M₃ : Type u_11} [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_8} {M₂ : Type u_10} [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_5} {M : Type u_8} {M₃ : Type u_11} [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_5} {M : Type u_8} {M₃ : Type u_11} [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_8) (M₂ : Type u_10) [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_14) (S : Type u_15) [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.toIntModule, allowing z • to be moved even if S 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 100]
                                                    instance LinearMap.IsScalarTower.compatibleSMul {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_14} {S : Type u_15} [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₂] :
                                                    CompatibleSMul M M₂ R S
                                                    instance LinearMap.IsScalarTower.compatibleSMul' {M : Type u_8} [AddCommMonoid M] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R S] [IsScalarTower R S M] :
                                                    @[simp]
                                                    theorem LinearMap.map_smul_of_tower {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
                                                    fₗ (c x) = c fₗ x
                                                    theorem LinearMapClass.map_smul_of_tower {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] {R : Type u_14} {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] {F : Type u_16} [LinearMap.CompatibleSMul M M₂ R S] [FunLike F M M₂] [LinearMapClass F S M M₂] (fₗ : F) (c : R) (x : M) :
                                                    fₗ (c x) = c fₗ x
                                                    theorem LinearMap.isScalarTower_of_injective {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (R : Type u_14) {S : Type u_15} [Semiring S] [SMul R M] [Module S M] [SMul R M₂] [Module S M₂] [SMul R S] [CompatibleSMul M M₂ R S] [IsScalarTower R S M₂] (f : M →ₗ[S] M₂) (hf : Function.Injective f) :
                                                    @[simp]
                                                    theorem map_zsmul_unit {F : Type u_16} {M : Type u_17} {N : Type u_18} [AddGroup M] [AddGroup N] [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (c : ˣ) (m : M) :
                                                    f (c m) = c f m
                                                    theorem LinearMap.isLinearMap_of_compatibleSMul (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
                                                    def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [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_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
                                                        f.toAddMonoidHom = f
                                                        def LinearMap.restrictScalars (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [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
                                                          Instances For
                                                            instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [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_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
                                                              (R f) = f
                                                              theorem LinearMap.restrictScalars_apply (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [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_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] :
                                                              @[simp]
                                                              theorem LinearMap.restrictScalars_inj (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] (fₗ gₗ : M →ₗ[S] M₂) :
                                                              R fₗ = R gₗ fₗ = gₗ
                                                              theorem LinearMap.toAddMonoidHom_injective {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid M₃] [Module R M] [Module S M₃] {σ : R →+* S} :
                                                              theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_5} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : R →+* S} {f 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} {S : Type u_5} {M₃ : Type u_11} [Semiring R] [Semiring S] [AddCommMonoid M₃] [Module S M₃] {σ : R →+* S} {f g : R →ₛₗ[σ] M₃} :
                                                              f = g f 1 = g 1
                                                              def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) :

                                                              Interpret a RingHom f as an f-semilinear map.

                                                              Equations
                                                                Instances For
                                                                  @[simp]
                                                                  theorem RingHom.toSemilinearMap_apply {R : Type u_1} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) (a✝ : R) :
                                                                  f.toSemilinearMap a✝ = (↑f).toFun a✝
                                                                  @[simp]
                                                                  theorem RingHom.coe_toSemilinearMap {R : Type u_1} {S : Type u_5} [Semiring R] [Semiring S] (f : R →+* S) :
                                                                  f.toSemilinearMap = f
                                                                  def LinearMap.comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [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
                                                                    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
                                                                        Instances For

                                                                          Pretty printer defined by notation3 command.

                                                                          Equations
                                                                            Instances For

                                                                              Composition of two linear maps is a linear map

                                                                              Equations
                                                                                Instances For
                                                                                  theorem LinearMap.comp_apply {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [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₁) :
                                                                                  (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_9} {M₂ : Type u_10} {M₃ : Type u_11} [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 ∘ₛₗ g) = f g
                                                                                  @[simp]
                                                                                  theorem LinearMap.comp_id {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
                                                                                  @[simp]
                                                                                  theorem LinearMap.id_comp {R₂ : Type u_3} {R₃ : Type u_4} {M₂ : Type u_10} {M₃ : Type u_11} [Semiring R₂] [Semiring R₃] [AddCommMonoid M₂] [AddCommMonoid M₃] {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₂₃ : R₂ →+* R₃} (f : M₂ →ₛₗ[σ₂₃] M₃) :
                                                                                  theorem LinearMap.comp_assoc {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [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_14} {M₄ : Type u_15} [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_9} {M₂ : Type u_10} {M₃ : Type u_11} [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 : Surjective g) :
                                                                                  Injective fun (f : M₂ →ₛₗ[σ₂₃] M₃) => 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_9} {M₂ : Type u_10} {M₃ : Type u_11} [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) :
                                                                                  f ∘ₛₗ g = f' ∘ₛₗ g f = f'
                                                                                  theorem Function.Injective.injective_linearMapComp_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [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 : Injective f) :
                                                                                  Injective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => f ∘ₛₗ g

                                                                                  The linear map version of Function.Injective.comp_left

                                                                                  theorem LinearMap.surjective_comp_left_of_exists_rightInverse {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [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₃} {σ₃₂ : R₃ →+* R₂} [RingHomInvPair σ₂₃ σ₃₂] [RingHomCompTriple σ₁₃ σ₃₂ σ₁₂] (hf : ∃ (f' : M₃ →ₛₗ[σ₃₂] M₂), f ∘ₛₗ f' = id) :
                                                                                  Function.Surjective fun (g : M₁ →ₛₗ[σ₁₂] M₂) => f ∘ₛₗ g
                                                                                  @[simp]
                                                                                  theorem LinearMap.cancel_left {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_9} {M₂ : Type u_10} {M₃ : Type u_11} [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 g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : Function.Injective f) :
                                                                                  f ∘ₛₗ g = f ∘ₛₗ g' g = g'
                                                                                  def LinearMap.inverse {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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
                                                                                    Instances For
                                                                                      theorem LinearMap.injective_of_comp_eq_id {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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 : g ∘ₛₗ f = id) :
                                                                                      theorem LinearMap.surjective_of_comp_eq_id {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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 : g ∘ₛₗ f = id) :
                                                                                      theorem LinearMap.map_neg {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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_5} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [Semiring S] [AddCommGroup M] [AddCommGroup M₂] {module_M : Module R M} {module_M₂ : Module S M₂} {σ : R →+* S} (f : M →ₛₗ[σ] M₂) (x y : M) :
                                                                                      f (x - y) = f x - f y
                                                                                      instance LinearMap.CompatibleSMul.intModule {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] {S : Type u_14} [Semiring S] [Module S M] [Module S M₂] :
                                                                                      instance LinearMap.CompatibleSMul.units {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_14} {S : Type u_15} [Monoid R] [MulAction R M] [MulAction R M₂] [Semiring S] [Module S M] [Module S M₂] [CompatibleSMul M M₂ R S] :
                                                                                      CompatibleSMul M M₂ Rˣ S
                                                                                      def Module.compHom.toLinearMap {R : Type u_14} {S : Type u_15} [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
                                                                                          @[simp]
                                                                                          theorem Module.compHom.toLinearMap_apply {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] (g : R →+* S) (a : R) :
                                                                                          (toLinearMap g) a = g a
                                                                                          @[deprecated "No deprecation message was provided." (since := "2024-11-08")]
                                                                                          def DistribMulActionHom.toSemilinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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
                                                                                            Instances For
                                                                                              instance DistribMulActionHom.instSemilinearMapClass {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} :
                                                                                              SemilinearMapClass (M →ₑ+[σ] M₂) σ M M₂
                                                                                              @[deprecated "No deprecation message was provided." (since := "2024-11-08")]
                                                                                              def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_8} {M₃ : Type u_11} [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.instLinearMapClassId {R : Type u_1} {M : Type u_8} {M₃ : Type u_11} [AddCommMonoid M] [AddCommMonoid M₃] [Semiring R] [Module R M] [Module R M₃] :
                                                                                                  LinearMapClass (M →+[R] M₃) R M M₃

                                                                                                  A DistribMulActionHom between two modules is a linear map.

                                                                                                  @[simp]
                                                                                                  theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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_5} {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] [Semiring R] [Module R M] [Semiring S] [Module S M₂] {σ : R →+* S} {f g : M →ₑ+[σ] M₂} (h : f = g) :
                                                                                                  f = g
                                                                                                  def IsLinearMap.mk' {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] (f : MM₂) (lin : IsLinearMap R f) :
                                                                                                  M →ₗ[R] M₂

                                                                                                  Convert an IsLinearMap predicate to a LinearMap

                                                                                                  Equations
                                                                                                    Instances For
                                                                                                      @[simp]
                                                                                                      theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [Semiring R] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R M₂] {f : MM₂} (lin : IsLinearMap R f) (x : M) :
                                                                                                      (mk' f lin) x = f x
                                                                                                      theorem IsLinearMap.isLinearMap_smul {R : Type u_14} {M : Type u_15} [CommSemiring R] [AddCommMonoid M] [Module R M] (c : R) :
                                                                                                      IsLinearMap R fun (z : M) => c z
                                                                                                      theorem IsLinearMap.isLinearMap_smul' {R : Type u_14} {M : Type u_15} [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_8} {M₂ : Type u_10} [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_8} [Semiring R] [AddCommGroup M] [Module R M] :
                                                                                                      IsLinearMap R fun (z : M) => -z
                                                                                                      theorem IsLinearMap.map_neg {R : Type u_1} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} [Semiring R] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R M₂] {f : MM₂} (lin : IsLinearMap R f) (x y : M) :
                                                                                                      f (x - y) = f x - f y
                                                                                                      def AddMonoidHom.toNatLinearMap {M : Type u_8} {M₂ : Type u_10} [AddCommMonoid M] [AddCommMonoid M₂] (f : M →+ M₂) :

                                                                                                      Reinterpret an additive homomorphism as an -linear map.

                                                                                                      Equations
                                                                                                        Instances For
                                                                                                          def AddMonoidHom.toIntLinearMap {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :

                                                                                                          Reinterpret an additive homomorphism as a -linear map.

                                                                                                          Equations
                                                                                                            Instances For
                                                                                                              @[simp]
                                                                                                              theorem AddMonoidHom.coe_toIntLinearMap {M : Type u_8} {M₂ : Type u_10} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
                                                                                                              f.toIntLinearMap = f
                                                                                                              instance LinearMap.instSMul {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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
                                                                                                                @[simp]
                                                                                                                theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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_5} {M : Type u_8} {M₂ : Type u_10} [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.instSMulCommClass {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [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₂)
                                                                                                                instance LinearMap.instIsScalarTower {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {T : Type u_7} {M : Type u_8} {M₂ : Type u_10} [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₂)
                                                                                                                instance LinearMap.instIsCentralScalar {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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₂)

                                                                                                                Arithmetic on the codomain #

                                                                                                                instance LinearMap.instZero {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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
                                                                                                                  @[simp]
                                                                                                                  theorem LinearMap.zero_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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_8} {M₂ : Type u_10} {M₃ : Type u_11} [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₃) :
                                                                                                                  g ∘ₛₗ 0 = 0
                                                                                                                  @[simp]
                                                                                                                  theorem LinearMap.zero_comp {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [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₂) :
                                                                                                                  0 ∘ₛₗ f = 0
                                                                                                                  instance LinearMap.instInhabited {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                                                                                  Inhabited (M →ₛₗ[σ₁₂] M₂)
                                                                                                                  Equations
                                                                                                                    @[simp]
                                                                                                                    theorem LinearMap.default_def {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                                                                                    instance LinearMap.uniqueOfLeft {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} [Subsingleton M] :
                                                                                                                    Unique (M →ₛₗ[σ₁₂] M₂)
                                                                                                                    Equations
                                                                                                                      instance LinearMap.uniqueOfRight {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} [Subsingleton M₂] :
                                                                                                                      Unique (M →ₛₗ[σ₁₂] M₂)
                                                                                                                      Equations
                                                                                                                        theorem LinearMap.ne_zero_of_injective {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} [Nontrivial M] {f : M →ₛₗ[σ₁₂] M₂} (hf : Function.Injective f) :
                                                                                                                        f 0
                                                                                                                        theorem LinearMap.ne_zero_of_surjective {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} [Nontrivial M₂] {f : M →ₛₗ[σ₁₂] M₂} (hf : Function.Surjective f) :
                                                                                                                        f 0
                                                                                                                        instance LinearMap.instAdd {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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
                                                                                                                          @[simp]
                                                                                                                          theorem LinearMap.add_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f 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_8} {M₂ : Type u_10} {M₃ : Type u_11} [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 h : M₂ →ₛₗ[σ₂₃] M₃) :
                                                                                                                          (h + g) ∘ₛₗ f = h ∘ₛₗ f + g ∘ₛₗ f
                                                                                                                          theorem LinearMap.comp_add {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [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 g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
                                                                                                                          h ∘ₛₗ (f + g) = h ∘ₛₗ f + h ∘ₛₗ g
                                                                                                                          instance LinearMap.addCommMonoid {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [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.instNeg {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [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
                                                                                                                              @[simp]
                                                                                                                              theorem LinearMap.neg_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [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_8} {M₂ : Type u_10} {N₃ : Type u_13} [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_8} {N₂ : Type u_12} {N₃ : Type u_13} [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.instSub {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [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
                                                                                                                                @[simp]
                                                                                                                                theorem LinearMap.sub_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommGroup N₂] [Module R₁ M] [Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f 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_8} {M₂ : Type u_10} {N₃ : Type u_13} [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 h : M₂ →ₛₗ[σ₂₃] N₃) :
                                                                                                                                (g - h) ∘ₛₗ f = g ∘ₛₗ f - h ∘ₛₗ f
                                                                                                                                theorem LinearMap.comp_sub {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_8} {N₂ : Type u_12} {N₃ : Type u_13} [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 g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
                                                                                                                                h ∘ₛₗ (g - f) = h ∘ₛₗ g - h ∘ₛₗ f
                                                                                                                                instance LinearMap.addCommGroup {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [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
                                                                                                                                  def LinearMap.evalAddMonoidHom {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (a : M) :
                                                                                                                                  (M →ₛₗ[σ₁₂] M₂) →+ M₂

                                                                                                                                  Evaluation of a σ₁₂-linear map at a fixed a, as an AddMonoidHom.

                                                                                                                                  Equations
                                                                                                                                    Instances For
                                                                                                                                      @[simp]
                                                                                                                                      theorem LinearMap.evalAddMonoidHom_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (a : M) (f : M →ₛₗ[σ₁₂] M₂) :
                                                                                                                                      def LinearMap.toAddMonoidHom' {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
                                                                                                                                      (M →ₛₗ[σ₁₂] M₂) →+ M →+ M₂

                                                                                                                                      LinearMap.toAddMonoidHom promoted to an AddMonoidHom.

                                                                                                                                      Equations
                                                                                                                                        Instances For
                                                                                                                                          @[simp]
                                                                                                                                          theorem LinearMap.toAddMonoidHom'_apply {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {M₂ : Type u_10} [Semiring R₁] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R₁ M] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] M₂) :
                                                                                                                                          @[simp]
                                                                                                                                          theorem LinearMap.identityMapOfZeroModuleIsZero {R₁ : Type u_2} {M : Type u_8} [Semiring R₁] [AddCommMonoid M] [Module R₁ M] [Subsingleton M] :
                                                                                                                                          id = 0

                                                                                                                                          If M is the zero module, then the identity map of M is the zero map.

                                                                                                                                          instance LinearMap.instDistribMulAction {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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_6} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [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₂) :
                                                                                                                                            (a g) ∘ₛₗ f = a g ∘ₛₗ f
                                                                                                                                            theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} {M₃ : Type u_11} [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₃] [CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
                                                                                                                                            g ∘ₗ (a f) = a g ∘ₗ f
                                                                                                                                            instance LinearMap.module {R : Type u_1} {R₂ : Type u_3} {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [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
                                                                                                                                              @[simp]
                                                                                                                                              theorem LinearMap.restrictScalars_zero (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] :
                                                                                                                                              R 0 = 0
                                                                                                                                              @[simp]
                                                                                                                                              theorem LinearMap.restrictScalars_add {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] (f g : M →ₗ[S] N) :
                                                                                                                                              R (f + g) = R f + R g
                                                                                                                                              @[simp]
                                                                                                                                              theorem LinearMap.restrictScalars_neg {R : Type u_14} {S : Type u_15} [Semiring R] [Semiring S] {M : Type u_19} {N : Type u_20} [AddCommMonoid M] [AddCommGroup N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] (f : M →ₗ[S] N) :
                                                                                                                                              R (-f) = -R f
                                                                                                                                              @[simp]
                                                                                                                                              theorem LinearMap.restrictScalars_smul {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] {R₁ : Type u_19} [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N] (c : R₁) (f : M →ₗ[S] N) :
                                                                                                                                              R (c f) = c R f
                                                                                                                                              @[simp]
                                                                                                                                              theorem LinearMap.restrictScalars_comp {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} {P : Type u_18} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] [AddCommMonoid P] [Module S P] [Module R P] [CompatibleSMul N P R S] [CompatibleSMul M P R S] (f : N →ₗ[S] P) (g : M →ₗ[S] N) :
                                                                                                                                              R (f ∘ₗ g) = R f ∘ₗ R g
                                                                                                                                              @[simp]
                                                                                                                                              theorem LinearMap.restrictScalars_trans {R : Type u_14} {S : Type u_15} {M : Type u_16} {N : Type u_17} [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] {T : Type u_20} [Semiring T] [Module T M] [Module T N] [CompatibleSMul M N S T] [CompatibleSMul M N R T] (f : M →ₗ[T] N) :
                                                                                                                                              R (S f) = R f
                                                                                                                                              def LinearMap.restrictScalarsₗ (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] (R₁ : Type u_19) [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N] :
                                                                                                                                              (M →ₗ[S] N) →ₗ[R₁] M →ₗ[R] N

                                                                                                                                              LinearMap.restrictScalars as a LinearMap.

                                                                                                                                              Equations
                                                                                                                                                Instances For
                                                                                                                                                  @[simp]
                                                                                                                                                  theorem LinearMap.restrictScalarsₗ_apply (R : Type u_14) (S : Type u_15) (M : Type u_16) (N : Type u_17) [Semiring R] [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] [Module S M] [Module S N] [CompatibleSMul M N R S] (R₁ : Type u_19) [Semiring R₁] [Module R₁ N] [SMulCommClass S R₁ N] [SMulCommClass R R₁ N] (fₗ : M →ₗ[S] N) :
                                                                                                                                                  (restrictScalarsₗ R S M N R₁) fₗ = R fₗ