Documentation

Mathlib.Algebra.Module.LinearMap

(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} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (f : MM₂) :
  • A linear map preserves addition.

    map_add : ∀ (x y : M), f (x + y) = f x + f y
  • A linear map preserves scalar multiplication.

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

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.

Instances For
    structure LinearMap {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (σ : R →+* S) (M : Type u_3) (M₂ : Type u_4) [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] extends AddHom :
    Type (maxu_3u_4)
    • A linear map preserves scalar multiplication. We prefer the spelling _root_.map_smul instead.

      map_smul' : ∀ (r : R) (x : M), AddHom.toFun toAddHom (r x) = σ r AddHom.toFun toAddHom x

    A map f between an R-module and an S-module over a ring homomorphism σ : R →+* S→+* 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₂→ₛₗ[σ] M₂) are bundled versions of such maps. For plain linear maps (i.e. for which σ = RingHom.id R), the notation M →ₗ[R] 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→ₛₗ[σ] N is the type of σ-semilinear maps from M to N.

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

      M →ₗ[R] N→ₗ[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.

      M →ₗ⋆[R] N→ₗ⋆[R] N⋆[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.
      class SemilinearMapClass (F : Type u_1) {R : outParam (Type u_2)} {S : outParam (Type u_3)} [inst : Semiring R] [inst : Semiring S] (σ : outParam (R →+* S)) (M : outParam (Type u_4)) (M₂ : outParam (Type u_5)) [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] extends AddHomClass :
      Type (max(maxu_1u_4)u_5)
      • A semilinear map preserves scalar multiplication up to some ring homomorphism σ. See also _root_.map_smul for the case where σ is the identity.

        map_smulₛₗ : ∀ (f : F) (r : R) (x : M), f (r x) = σ r f x

      SemilinearMapClass F σ M M₂ asserts F is a type of bundled σ-semilinear maps M → 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→+* 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]
        abbrev LinearMapClass (F : Type u_1) (R : outParam (Type u_2)) (M : outParam (Type u_3)) (M₂ : outParam (Type u_4)) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] :
        Type (max(maxu_1u_3)u_4)

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

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

        Equations
        instance SemilinearMapClass.addMonoidHomClass {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} (F : Type u_5) :
        {x : Semiring R} → {x_1 : Semiring S} → {x_2 : AddCommMonoid M} → {x_3 : AddCommMonoid M₃} → {x_4 : Module R M} → {x_5 : Module S M₃} → {σ : R →+* S} → [inst : SemilinearMapClass F σ M M₃] → AddMonoidHomClass F M M₃
        Equations
        instance SemilinearMapClass.distribMulActionHomClass {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} (F : Type u_4) :
        {x : Semiring R} → {x_1 : AddCommMonoid M} → {x_2 : AddCommMonoid M₂} → {x_3 : Module R M} → {x_4 : Module R M₂} → [inst : LinearMapClass F R M M₂] → DistribMulActionHomClass F R M M₂
        Equations
        • One or more equations did not get rendered due to their size.
        theorem SemilinearMapClass.map_smul_inv {R : Type u_2} {S : Type u_1} {M : Type u_5} {M₃ : Type u_3} {F : Type u_4} :
        ∀ {x : Semiring R} {x_1 : Semiring S} {x_2 : AddCommMonoid M} {x_3 : AddCommMonoid M₃} {x_4 : Module R M} {x_5 : Module S M₃} {σ : R →+* S} (f : F) [i : SemilinearMapClass F σ M M₃] {σ' : S →+* R} [inst : RingHomInvPair σ σ'] (c : S) (x_6 : M), c f x_6 = f (σ' c x_6)
        instance LinearMap.instSemilinearMapClassLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
        SemilinearMapClass (M →ₛₗ[σ] M₃) σ M M₃
        Equations
        instance LinearMap.instFunLikeLinearMap {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
        FunLike (M →ₛₗ[σ] M₃) M fun x => M₃
        Equations
        • LinearMap.instFunLikeLinearMap = let src := AddHomClass.toFunLike; { coe := FunLike.coe, coe_injective' := (_ : Function.Injective FunLike.coe) }
        def LinearMap.toDistribMulActionHom {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (f : M →ₗ[R] M₂) :
        M →+[R] M₂

        The DistribMulActionHom underlying a LinearMap.

        Equations
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem LinearMap.coe_toAddHom {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
        f.toAddHom = f
        theorem LinearMap.toFun_eq_coe {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} {f : M →ₛₗ[σ] M₃} :
        f.toAddHom.toFun = f
        theorem LinearMap.ext {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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
        • One or more equations did not get rendered due to their size.
        @[simp]
        theorem LinearMap.coe_copy {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r x) = σ r AddHom.toFun f x) :
        { toAddHom := f, map_smul' := h } = f
        @[simp]
        theorem LinearMap.coe_addHom_mk {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : AddHom M M₃) (h : ∀ (r : R) (x : M), AddHom.toFun f (r x) = σ r AddHom.toFun f x) :
        { toAddHom := f, map_smul' := h } = f
        def LinearMap.id {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

        Identity map as a LinearMap

        Equations
        • One or more equations did not get rendered due to their size.
        theorem LinearMap.id_apply {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
        LinearMap.id x = x
        @[simp]
        theorem LinearMap.id_coe {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
        LinearMap.id = id
        theorem LinearMap.isLinear {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (fₗ : M →ₗ[R] M₂) :
        IsLinearMap R fₗ
        theorem LinearMap.coe_injective {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
        Function.Injective FunLike.coe
        theorem LinearMap.congr_arg {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : ∀ (r : R) (x : M), AddHom.toFun (f) (r x) = σ r AddHom.toFun (f) x) :
        { toAddHom := f, map_smul' := h } = f
        theorem LinearMap.map_add {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_3} {S : Type u_4} {M : Type u_2} {M₃ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
        f 0 = 0
        theorem LinearMap.map_smulₛₗ {R : Type u_2} {S : Type u_4} {M : Type u_3} {M₃ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : 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_2} {M : Type u_3} {M₂ : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : 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_2} {S : Type u_1} {M : Type u_4} {M₃ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) {σ' : S →+* R} [inst : RingHomInvPair σ σ'] (c : S) (x : M) :
        c f x = f (σ' c x)
        @[simp]
        theorem LinearMap.map_eq_zero_iff {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) (h : Function.Injective f) {x : M} :
        f x = 0 x = 0
        @[simp]
        theorem image_smul_setₛₗ {R : Type u_2} {S : Type u_3} (M : Type u_4) (M₃ : Type u_5) [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] (σ : R →+* S) {F : Type u_1} (h : F) [inst : SemilinearMapClass F σ M M₃] (c : R) (s : Set M) :
        h '' (c s) = σ c h '' s
        theorem preimage_smul_setₛₗ {R : Type u_2} {S : Type u_3} (M : Type u_4) (M₃ : Type u_5) [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] (σ : R →+* S) {F : Type u_1} (h : F) [inst : SemilinearMapClass F σ M M₃] {c : R} (hc : IsUnit c) (s : Set M₃) :
        h ⁻¹' (σ c s) = c h ⁻¹' s
        theorem image_smul_set (R : Type u_2) (M : Type u_3) (M₂ : Type u_4) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] {F : Type u_1} (h : F) [inst : LinearMapClass F R M M₂] (c : R) (s : Set M) :
        h '' (c s) = c h '' s
        theorem preimage_smul_set (R : Type u_2) (M : Type u_3) (M₂ : Type u_4) [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] {F : Type u_1} (h : F) [inst : LinearMapClass F R M M₂] {c : R} (hc : IsUnit c) (s : Set M₂) :
        h ⁻¹' (c s) = c h ⁻¹' s
        class LinearMap.CompatibleSMul (M : Type u_1) (M₂ : Type u_2) [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] (R : Type u_3) (S : Type u_4) [inst : Semiring S] [inst : SMul R M] [inst : Module S M] [inst : SMul R M₂] [inst : Module S M₂] :
        • Scalar multiplication by R of M can be moved through linear maps.

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

        A typeclass for has_smul structures which can be moved through a LinearMap. This typeclass is generated automatically from a 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.

        Instances
          instance LinearMap.IsScalarTower.compatibleSMul {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] {R : Type u_3} {S : Type u_4} [inst : Semiring S] [inst : SMul R S] [inst : SMul R M] [inst : Module S M] [inst : IsScalarTower R S M] [inst : SMul R M₂] [inst : Module S M₂] [inst : IsScalarTower R S M₂] :
          Equations
          • LinearMap.IsScalarTower.compatibleSMul = { map_smul := (_ : ∀ (fₗ : M →ₗ[S] M₂) (c : R) (x : M), fₗ (c x) = c fₗ x) }
          @[simp]
          theorem LinearMap.map_smul_of_tower {M : Type u_3} {M₂ : Type u_4} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst : SMul R M] [inst : Module S M] [inst : SMul R M₂] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (c : R) (x : M) :
          fₗ (c x) = c fₗ x
          def LinearMap.toAddMonoidHom {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
          M →+ M₃

          convert a linear map to an additive map

          Equations
          • LinearMap.toAddMonoidHom f = { toZeroHom := { toFun := f, map_zero' := (_ : f 0 = 0) }, map_add' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }
          @[simp]
          theorem LinearMap.toAddMonoidHom_coe {R : Type u_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} (f : M →ₛₗ[σ] M₃) :
          def LinearMap.restrictScalars (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : 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' := (_ : ∀ (x y : M), fₗ (x + y) = fₗ x + fₗ y) }, map_smul' := (_ : ∀ (c : R) (x : M), fₗ (c x) = c fₗ x) }
          instance LinearMap.coeIsScalarTower (R : Type u_1) {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] :
          CoeHTCT (M →ₗ[S] M₂) (M →ₗ[R] M₂)
          Equations
          @[simp]
          theorem LinearMap.coe_restrictScalars (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (f : M →ₗ[S] M₂) :
          ↑(R f) = f
          theorem LinearMap.restrictScalars_apply (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] (fₗ : M →ₗ[S] M₂) (x : M) :
          ↑(R fₗ) x = fₗ x
          theorem LinearMap.restrictScalars_injective (R : Type u_4) {S : Type u_3} {M : Type u_1} {M₂ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] :
          @[simp]
          theorem LinearMap.restrictScalars_inj (R : Type u_4) {S : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] [inst : Module S M] [inst : Module S M₂] [inst : 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_3} {S : Type u_4} {M : Type u_1} {M₃ : Type u_2} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module S M₃] {σ : R →+* S} :
          Function.Injective LinearMap.toAddMonoidHom
          theorem LinearMap.ext_ring {R : Type u_1} {S : Type u_2} {M₃ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M₃] [inst : 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_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : 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_2} {M₃ : Type u_3} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M₃] [inst : 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_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) (a : R) :
          ↑(RingHom.toSemilinearMap f) a = f a
          def RingHom.toSemilinearMap {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R →+* S) :

          Interpret a RingHom f as an f-semilinear map.

          Equations
          • One or more equations did not get rendered due to their size.
          def LinearMap.comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M₂ →ₛₗ[σ₂₃] M₃) (g : M₁ →ₛₗ[σ₁₂] M₂) :
          M₁ →ₛₗ[σ₁₃] M₃

          Composition of two linear maps is a linear map

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

          ∘ₗ∘ₗ 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
          theorem LinearMap.comp_apply {R₁ : Type u_3} {R₂ : Type u_5} {R₃ : Type u_4} {M₁ : Type u_2} {M₂ : Type u_6} {M₃ : Type u_1} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : 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_3} {R₂ : Type u_5} {R₃ : Type u_4} {M₁ : Type u_1} {M₂ : Type u_6} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : 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_1} {M₃ : Type u_2} [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₂] [inst : 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_1} {M₃ : Type u_2} [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₂] [inst : 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.cancel_right {R₁ : Type u_3} {R₂ : Type u_4} {R₃ : Type u_6} {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_5} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {f' : M₂ →ₛₗ[σ₂₃] M₃} (hg : Function.Surjective g) :
          theorem LinearMap.cancel_left {R₁ : Type u_6} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_5} {M₂ : Type u_1} {M₃ : Type u_2} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M₁] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃} {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {f : M₂ →ₛₗ[σ₂₃] M₃} {g : M₁ →ₛₗ[σ₁₂] M₂} {g' : M₁ →ₛₗ[σ₁₂] M₂} (hf : Function.Injective f) :
          def LinearMap.inverse {R : Type u_1} {S : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring S] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module S M₂] {σ : R →+* S} {σ' : S →+* R} [inst : 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
          • One or more equations did not get rendered due to their size.
          theorem LinearMap.map_neg {R : Type u_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommGroup M] [inst : 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_3} {S : Type u_4} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : Semiring S] [inst : AddCommGroup M] [inst : 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_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] {S : Type u_3} [inst : Semiring S] [inst : Module S M] [inst : Module S M₂] :
          Equations
          • LinearMap.CompatibleSMul.intModule = { map_smul := (_ : ∀ (fₗ : M →ₗ[S] M₂) (c : ) (x : M), fₗ (c x) = c fₗ x) }
          instance LinearMap.CompatibleSMul.units {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] {R : Type u_3} {S : Type u_4} [inst : Monoid R] [inst : MulAction R M] [inst : MulAction R M₂] [inst : Semiring S] [inst : Module S M] [inst : Module S M₂] [inst : LinearMap.CompatibleSMul M M₂ R S] :
          Equations
          • LinearMap.CompatibleSMul.units = { map_smul := (_ : ∀ (fₗ : M →ₗ[S] M₂) (c : Rˣ) (x : M), fₗ (c x) = c fₗ x) }
          @[simp]
          theorem Module.compHom.toLinearMap_apply {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (g : R →+* S) (a : R) :
          def Module.compHom.toLinearMap {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (g : R →+* S) :

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

          Equations
          • Module.compHom.toLinearMap g = { toAddHom := { toFun := g, map_add' := (_ : ∀ (a b : R), g (a + b) = g a + g b) }, map_smul' := (_ : ∀ (a b : R), g (a * b) = g a * g b) }
          def DistribMulActionHom.toLinearMap {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (fₗ : M →+[R] M₂) :
          M →ₗ[R] M₂

          A DistribMulActionHom between two modules is a linear map.

          Equations
          • One or more equations did not get rendered due to their size.
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem DistribMulActionHom.coe_toLinearMap {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] (f : M →+[R] M₂) :
          f = f
          theorem DistribMulActionHom.toLinearMap_injective {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] {f : M →+[R] M₂} {g : M →+[R] M₂} (h : f = g) :
          f = g
          def IsLinearMap.mk' {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : 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' := (_ : ∀ (x y : M), f (x + y) = f x + f y) }, map_smul' := (_ : ∀ (c : R) (x : M), f (c x) = c f x) }
          @[simp]
          theorem IsLinearMap.mk'_apply {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : 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_1} {M : Type u_2} [inst : CommSemiring R] [inst : AddCommMonoid M] [inst : Module R M] (c : R) :
          IsLinearMap R fun z => c z
          theorem IsLinearMap.isLinearMap_smul' {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (a : M) :
          IsLinearMap R fun c => c a
          theorem IsLinearMap.map_zero {R : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (lin : IsLinearMap R f) :
          f 0 = 0
          theorem IsLinearMap.isLinearMap_neg {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommGroup M] [inst : Module R M] :
          IsLinearMap R fun z => -z
          theorem IsLinearMap.map_neg {R : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : AddCommGroup M] [inst : AddCommGroup M₂] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (lin : IsLinearMap R f) (x : M) :
          f (-x) = -f x
          theorem IsLinearMap.map_sub {R : Type u_3} {M : Type u_2} {M₂ : Type u_1} [inst : Semiring R] [inst : AddCommGroup M] [inst : AddCommGroup M₂] [inst : Module R M] [inst : Module R M₂] {f : MM₂} (lin : IsLinearMap R f) (x : M) (y : M) :
          f (x - y) = f x - f y
          @[inline]
          abbrev Module.End (R : Type u) (M : Type v) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

          Linear endomorphisms of a module, with associated ring structure Module.End.semiring and algebra structure Module.End.algebra.

          Equations
          def AddMonoidHom.toNatLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] (f : M →+ M₂) :

          Reinterpret an additive homomorphism as a -linear map.

          Equations
          theorem AddMonoidHom.toNatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] :
          Function.Injective AddMonoidHom.toNatLinearMap
          def AddMonoidHom.toIntLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : AddCommGroup M₂] (f : M →+ M₂) :

          Reinterpret an additive homomorphism as a -linear map.

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

          Reinterpret an additive homomorphism as a -linear map.

          Equations
          • One or more equations did not get rendered due to their size.
          theorem AddMonoidHom.toRatLinearMap_injective {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : Module M] [inst : AddCommGroup M₂] [inst : Module M₂] :
          Function.Injective AddMonoidHom.toRatLinearMap
          @[simp]
          theorem AddMonoidHom.coe_toRatLinearMap {M : Type u_1} {M₂ : Type u_2} [inst : AddCommGroup M] [inst : Module M] [inst : AddCommGroup M₂] [inst : Module M₂] (f : M →+ M₂) :
          instance LinearMap.instSMulLinearMap {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : SMulCommClass R₂ S M₂] :
          SMul S (M →ₛₗ[σ₁₂] M₂)
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem LinearMap.smul_apply {R : Type u_1} {R₂ : Type u_2} {S : Type u_5} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : 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_2} {S : Type u_5} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : SMulCommClass R₂ S M₂] (a : S) (f : M →ₛₗ[σ₁₂] M₂) :
          ↑(a f) = a f
          instance LinearMap.instSMulCommClassLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : SMulCommClass R₂ S M₂] [inst : Monoid T] [inst : DistribMulAction T M₂] [inst : SMulCommClass R₂ T M₂] [inst : SMulCommClass S T M₂] :
          SMulCommClass S T (M →ₛₗ[σ₁₂] M₂)
          Equations
          instance LinearMap.instIsScalarTowerLinearMapInstSMulLinearMapInstSMulLinearMap {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {T : Type u_4} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : SMulCommClass R₂ S M₂] [inst : Monoid T] [inst : DistribMulAction T M₂] [inst : SMulCommClass R₂ T M₂] [inst : SMul S T] [inst : IsScalarTower S T M₂] :
          IsScalarTower S T (M →ₛₗ[σ₁₂] M₂)
          Equations
          instance LinearMap.instIsCentralScalarLinearMapInstSMulLinearMapMulOppositeMonoid {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : SMulCommClass R₂ S M₂] [inst : DistribMulAction Sᵐᵒᵖ M₂] [inst : SMulCommClass R₂ Sᵐᵒᵖ M₂] [inst : IsCentralScalar S M₂] :
          IsCentralScalar S (M →ₛₗ[σ₁₂] M₂)
          Equations

          Arithmetic on the codomain #

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

          The constant 0 map is linear.

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

          The sum of two linear maps is linear.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem LinearMap.add_apply {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R₁ M] [inst : 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_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] M₃) (h : M₂ →ₛₗ[σ₂₃] M₃) :
          theorem LinearMap.comp_add {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {M₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M →ₛₗ[σ₁₂] M₂) (h : M₂ →ₛₗ[σ₂₃] M₃) :
          instance LinearMap.addCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R₁ M] [inst : Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} :
          AddCommMonoid (M →ₛₗ[σ₁₂] M₂)

          The type of linear maps is an additive monoid.

          Equations
          • One or more equations did not get rendered due to their size.
          instance LinearMap.instNegLinearMapToAddCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
          Neg (M →ₛₗ[σ₁₂] N₂)

          The negation of a linear map is linear.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem LinearMap.neg_apply {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} (f : M →ₛₗ[σ₁₂] N₂) (x : M) :
          ↑(-f) x = -f x
          @[simp]
          theorem LinearMap.neg_comp {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommGroup N₃] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) :
          @[simp]
          theorem LinearMap.comp_neg {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {N₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : AddCommGroup N₃] [inst : Module R₁ M] [inst : Module R₂ N₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : N₂ →ₛₗ[σ₂₃] N₃) :
          instance LinearMap.instSubLinearMapToAddCommMonoid {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
          Sub (M →ₛₗ[σ₁₂] N₂)

          The subtraction of two linear maps is linear.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem LinearMap.sub_apply {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : Module R₁ M] [inst : 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_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {M₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommGroup N₃] [inst : Module R₁ M] [inst : Module R₂ M₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] M₂) (g : M₂ →ₛₗ[σ₂₃] N₃) (h : M₂ →ₛₗ[σ₂₃] N₃) :
          theorem LinearMap.comp_sub {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_5} {M : Type u_3} {N₂ : Type u_4} {N₃ : Type u_6} [inst : Semiring R₁] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : AddCommGroup N₃] [inst : Module R₁ M] [inst : Module R₂ N₂] [inst : Module R₃ N₃] {σ₁₂ : R₁ →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (f : M →ₛₗ[σ₁₂] N₂) (g : M →ₛₗ[σ₁₂] N₂) (h : N₂ →ₛₗ[σ₂₃] N₃) :
          instance LinearMap.addCommGroup {R₁ : Type u_1} {R₂ : Type u_2} {M : Type u_3} {N₂ : Type u_4} [inst : Semiring R₁] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommGroup N₂] [inst : Module R₁ M] [inst : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂} :
          AddCommGroup (M →ₛₗ[σ₁₂] N₂)

          The type of linear maps is an additive group.

          Equations
          • One or more equations did not get rendered due to their size.
          instance LinearMap.instDistribMulActionLinearMapToAddMonoidAddCommMonoid {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : SMulCommClass R₂ S M₂] :
          DistribMulAction S (M →ₛₗ[σ₁₂] M₂)
          Equations
          theorem LinearMap.smul_comp {R : Type u_5} {R₂ : Type u_1} {R₃ : Type u_2} {S₃ : Type u_7} {M : Type u_6} {M₂ : Type u_3} {M₃ : Type u_4} [inst : Semiring R] [inst : Semiring R₂] [inst : Semiring R₃] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Module R₂ M₂] [inst : Module R₃ M₃] {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst : Monoid S₃] [inst : DistribMulAction S₃ M₃] [inst : SMulCommClass R₃ S₃ M₃] (a : S₃) (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂) :
          theorem LinearMap.comp_smul {R : Type u_1} {S : Type u_4} {M : Type u_5} {M₂ : Type u_2} {M₃ : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : AddCommMonoid M₃] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M₂] [inst : Module R M₂] [inst : Module R M₃] [inst : SMulCommClass R S M₂] [inst : DistribMulAction S M₃] [inst : SMulCommClass R S M₃] [inst : LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₃ →ₗ[R] M₂) (a : S) (f : M →ₗ[R] M₃) :
          instance LinearMap.instModuleLinearMapAddCommMonoid {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Semiring S] [inst : Module S M₂] [inst : SMulCommClass R₂ S M₂] :
          Module S (M →ₛₗ[σ₁₂] M₂)
          Equations
          instance LinearMap.instNoZeroSMulDivisorsLinearMapToZeroToMonoidWithZeroInstZeroLinearMapInstSMulLinearMapToMonoidToDistribMulAction {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst : Semiring R₂] [inst : AddCommMonoid M] [inst : AddCommMonoid M₂] [inst : Module R M] [inst : Module R₂ M₂] {σ₁₂ : R →+* R₂} [inst : Semiring S] [inst : Module S M₂] [inst : SMulCommClass R₂ S M₂] [inst : NoZeroSMulDivisors S M₂] :
          NoZeroSMulDivisors S (M →ₛₗ[σ₁₂] M₂)
          Equations
          • One or more equations did not get rendered due to their size.

          Monoid structure of endomorphisms #

          Lemmas about pow such as LinearMap.pow_apply appear in later files.

          instance LinearMap.instOneEnd {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
          Equations
          • LinearMap.instOneEnd = { one := LinearMap.id }
          instance LinearMap.instMulEnd {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
          Equations
          • LinearMap.instMulEnd = { mul := LinearMap.comp }
          theorem LinearMap.one_eq_id {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
          1 = LinearMap.id
          theorem LinearMap.mul_eq_comp {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (f : Module.End R M) (g : Module.End R M) :
          @[simp]
          theorem LinearMap.one_apply {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (x : M) :
          1 x = x
          @[simp]
          theorem LinearMap.mul_apply {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (f : Module.End R M) (g : Module.End R M) (x : M) :
          ↑(f * g) x = f (g x)
          theorem LinearMap.coe_one {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
          1 = id
          theorem LinearMap.coe_mul {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (f : Module.End R M) (g : Module.End R M) :
          ↑(f * g) = f g
          instance Module.End.monoid {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
          Equations
          instance Module.End.semiring {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :
          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem Module.End.natCast_apply {R : Type u_2} {M : Type u_1} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (n : ) (m : M) :
          n m = n m

          See also Module.End.natCast_def.

          instance Module.End.ring {R : Type u_1} {N₁ : Type u_2} [inst : Semiring R] [inst : AddCommGroup N₁] [inst : Module R N₁] :
          Ring (Module.End R N₁)
          Equations
          • Module.End.ring = let src := Module.End.semiring; let src_1 := LinearMap.addCommGroup; Ring.mk SubNegMonoid.zsmul (_ : ∀ (a : N₁ →ₗ[R] N₁), -a + a = 0)
          @[simp]
          theorem Module.End.intCast_apply {R : Type u_2} {N₁ : Type u_1} [inst : Semiring R] [inst : AddCommGroup N₁] [inst : Module R N₁] (z : ) (m : N₁) :
          z m = z m

          See also Module.End.intCast_def.

          instance Module.End.isScalarTower {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass R S M] :
          Equations
          instance Module.End.smulCommClass {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass R S M] [inst : SMul S R] [inst : IsScalarTower S R M] :
          Equations
          instance Module.End.smulCommClass' {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass R S M] [inst : SMul S R] [inst : IsScalarTower S R M] :
          Equations

          Action by a module endomorphism. #

          instance LinearMap.applyModule {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] :

          The tautological action by module.End R M (aka M →ₗ[R] M→ₗ[R] M) on M.

          This generalizes Function.End.applyMulAction.

          Equations
          • LinearMap.applyModule = Module.mk (_ : ∀ (f g : M →ₗ[R] M) (x : M), ↑(f + g) x = f x + g x) (_ : ∀ (x : M), 0 x = 0)
          @[simp]
          theorem LinearMap.smul_def {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] (f : Module.End R M) (a : M) :
          f a = f a

          Actions as module endomorphisms #

          @[simp]
          theorem DistribMulAction.toLinearMap_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :
          ∀ (a : M), ↑(DistribMulAction.toLinearMap R M s) a = SMul.smul s a
          def DistribMulAction.toLinearMap (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :

          Each element of the monoid defines a linear map.

          This is a stronger version of DistribMulAction.toAddMonoidHom.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem DistribMulAction.toModuleEnd_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] (s : S) :
          def DistribMulAction.toModuleEnd (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Monoid S] [inst : DistribMulAction S M] [inst : SMulCommClass S R M] :

          Each element of the monoid defines a module endomorphism.

          This is a stronger version of DistribMulAction.toAddMonoidEnd.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem Module.toModuleEnd_apply (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Semiring S] [inst : Module S M] [inst : SMulCommClass S R M] (s : S) :
          def Module.toModuleEnd (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst : AddCommMonoid M] [inst : Module R M] [inst : Semiring S] [inst : Module S M] [inst : SMulCommClass S R M] :

          Each element of the semiring defines a module endomorphism.

          This is a stronger version of DistribMulAction.toModuleEnd.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem Module.moduleEndSelf_symm_apply_unop (R : Type u_1) [inst : Semiring R] (f : Module.End R R) :
          (↑(RingEquiv.symm (Module.moduleEndSelf R)) f).unop = f 1

          The canonical (semi)ring isomorphism from Rᵐᵒᵖ to Module.End R R induced by the right multiplication.

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

          The canonical (semi)ring isomorphism from R to Module.End Rᵐᵒᵖ R induced by the left multiplication.

          Equations
          • One or more equations did not get rendered due to their size.
          theorem Module.End.natCast_def (R : Type u_2) {N₁ : Type u_1} [inst : Semiring R] (n : ) [inst : AddCommMonoid N₁] [inst : Module R N₁] :
          n = ↑(Module.toModuleEnd R N₁) n
          theorem Module.End.intCast_def (R : Type u_2) {N₁ : Type u_1} [inst : Semiring R] (z : ) [inst : AddCommGroup N₁] [inst : Module R N₁] :
          z = ↑(Module.toModuleEnd R N₁) z