Documentation

Mathlib.Algebra.Module.Submodule.Range

Range of linear maps #

The range LinearMap.range of a (semi)linear map f : M → M₂ is a submodule of M₂.

More specifically, LinearMap.range applies to any SemilinearMapClass over a RingHomSurjective ring homomorphism.

Note that this also means that dot notation (i.e. f.range for a linear map f) does not work.

Notations #

Tags #

linear algebra, vector space, module, range

def LinearMap.range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) :
Submodule R₂ M₂

The range of a linear map f : M → M₂ is a submodule of M₂. See Note [range copy pattern].

Equations
Instances For
    theorem LinearMap.range_coe {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) :
    theorem LinearMap.range_toAddSubmonoid {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
    @[simp]
    theorem LinearMap.mem_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {x : M₂} :
    x LinearMap.range f ∃ (y : M), f y = x
    theorem LinearMap.range_eq_map {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) :
    theorem LinearMap.mem_range_self {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) (x : M) :
    @[simp]
    theorem LinearMap.range_id {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] :
    LinearMap.range LinearMap.id =
    theorem LinearMap.range_comp {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [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 τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    theorem LinearMap.range_comp_le_range {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [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 τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) :
    theorem LinearMap.range_eq_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} :
    theorem LinearMap.range_le_iff_comap {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} :
    theorem LinearMap.map_le_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R M} :
    @[simp]
    theorem LinearMap.range_neg {R : Type u_12} {R₂ : Type u_13} {M : Type u_14} {M₂ : Type u_15} [Semiring R] [Ring R₂] [AddCommMonoid M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
    theorem LinearMap.range_domRestrict_le_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (S : Submodule R M) :
    LinearMap.range (f.domRestrict S) LinearMap.range f
    @[simp]
    theorem AddMonoidHom.coe_toIntLinearMap_range {M : Type u_12} {M₂ : Type u_13} [AddCommGroup M] [AddCommGroup M₂] (f : M →+ M₂) :
    LinearMap.range f.toIntLinearMap = AddSubgroup.toIntSubmodule f.range
    theorem Submodule.map_comap_eq_of_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {p : Submodule R₂ M₂} (h : p LinearMap.range f) :
    @[simp]
    theorem LinearMap.iterateRange_coe {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) (n : ) :
    f.iterateRange n = LinearMap.range (f ^ n)
    def LinearMap.iterateRange {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] M) :

    The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.

    Equations
    Instances For
      @[reducible, inline]
      abbrev LinearMap.rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
      M →ₛₗ[τ₁₂] (LinearMap.range f)

      Restrict the codomain of a linear map f to f.range.

      This is the bundled version of Set.rangeFactorization.

      Equations
      Instances For
        instance LinearMap.fintypeRange {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [Fintype M] [DecidableEq M₂] [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :

        The range of a linear map is finite if the domain is finite. Note: this instance can form a diamond with Subtype.fintype in the presence of Fintype M₂.

        Equations
        theorem LinearMap.range_codRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₂₁ : R₂ →+* R} [RingHomSurjective τ₂₁] (p : Submodule R M) (f : M₂ →ₛₗ[τ₂₁] M) (hf : ∀ (c : M₂), f c p) :
        theorem Submodule.map_comap_eq {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) (q : Submodule R₂ M₂) :
        theorem Submodule.map_comap_eq_self {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} {q : Submodule R₂ M₂} (h : q LinearMap.range f) :
        @[simp]
        theorem LinearMap.range_zero {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] :
        theorem LinearMap.range_le_bot_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
        theorem LinearMap.range_eq_bot {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} :
        theorem LinearMap.range_le_ker_iff {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [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 τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {g : M₂ →ₛₗ[τ₂₃] M₃} :
        theorem LinearMap.comap_le_comap_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} (hf : LinearMap.range f = ) {p : Submodule R₂ M₂} {p' : Submodule R₂ M₂} :
        theorem LinearMap.comap_injective {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] {f : F} (hf : LinearMap.range f = ) :
        theorem LinearMap.range_toAddSubgroup {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
        (LinearMap.range f).toAddSubgroup = f.toAddMonoidHom.range
        theorem LinearMap.ker_le_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Ring R] [Ring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} [RingHomSurjective τ₁₂] {p : Submodule R M} :
        LinearMap.ker f p yLinearMap.range f, f ⁻¹' {y} p
        theorem LinearMap.range_smul {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) (h : a 0) :
        theorem LinearMap.range_smul' {K : Type u_4} {V : Type u_9} {V₂ : Type u_10} [Semifield K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₂] [Module K V₂] (f : V →ₗ[K] V₂) (a : K) :
        LinearMap.range (a f) = ⨆ (_ : a 0), LinearMap.range f
        @[simp]
        theorem Submodule.map_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {F : Type u_11} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] [RingHomSurjective τ₁₂] (f : F) :
        @[simp]
        theorem Submodule.range_subtype {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        LinearMap.range p.subtype = p
        theorem Submodule.map_subtype_le {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R p) :
        Submodule.map p.subtype p' p
        theorem Submodule.map_subtype_top {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        Submodule.map p.subtype = p

        Under the canonical linear map from a submodule p to the ambient space M, the image of the maximal submodule of p is just p.

        @[simp]
        theorem Submodule.comap_subtype_eq_top {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} :
        Submodule.comap p.subtype p' = p p'
        @[simp]
        theorem Submodule.comap_subtype_self {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        Submodule.comap p.subtype p =
        theorem Submodule.range_inclusion {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R M) (h : p q) :
        @[simp]
        theorem Submodule.map_subtype_range_inclusion {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : p p') :
        def Submodule.MapSubtype.relIso {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        Submodule R p ≃o { p' : Submodule R M // p' p }

        If N ⊆ M then submodules of N are the same as submodules of M contained in N.

        See also Submodule.mapIic.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def Submodule.MapSubtype.orderEmbedding {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :

          If p ⊆ M is a submodule, the ordering of submodules of p is embedded in the ordering of submodules of M.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem Submodule.map_subtype_embedding_eq {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R p) :
            def Submodule.mapIic {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
            Submodule R p ≃o (Set.Iic p)

            If N ⊆ M then submodules of N are the same as submodules of M contained in N.

            Equations
            Instances For
              @[simp]
              theorem Submodule.coe_mapIic_apply {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (q : Submodule R p) :
              (p.mapIic q) = Submodule.map p.subtype q
              theorem LinearMap.ker_eq_bot_of_cancel {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {f : M →ₛₗ[τ₁₂] M₂} (h : ∀ (u v : (LinearMap.ker f) →ₗ[R] M), f.comp u = f.comp vu = v) :

              A monomorphism is injective.

              theorem LinearMap.range_comp_of_range_eq_top {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M : Type u_6} {M₂ : Type u_7} {M₃ : Type u_8} [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 τ₁₂ τ₂₃ τ₁₃] [RingHomSurjective τ₁₂] [RingHomSurjective τ₂₃] [RingHomSurjective τ₁₃] {f : M →ₛₗ[τ₁₂] M₂} (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : LinearMap.range f = ) :
              def LinearMap.submoduleImage {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_11} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} (ϕ : O →ₗ[R] M') (N : Submodule R M) :

              If O is a submodule of M, and Φ : O →ₗ M' is a linear map, then (ϕ : O →ₗ M').submoduleImage N is ϕ(N) as a submodule of M'

              Equations
              Instances For
                @[simp]
                theorem LinearMap.mem_submoduleImage {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_11} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} {ϕ : O →ₗ[R] M'} {N : Submodule R M} {x : M'} :
                x ϕ.submoduleImage N ∃ (y : M) (yO : y O), y N ϕ y, yO = x
                theorem LinearMap.mem_submoduleImage_of_le {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_11} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} {ϕ : O →ₗ[R] M'} {N : Submodule R M} (hNO : N O) {x : M'} :
                x ϕ.submoduleImage N ∃ (y : M) (yN : y N), ϕ y, = x
                theorem LinearMap.submoduleImage_apply_of_le {R : Type u_1} {M : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_11} [AddCommGroup M'] [Module R M'] {O : Submodule R M} (ϕ : O →ₗ[R] M') (N : Submodule R M) (hNO : N O) :
                ϕ.submoduleImage N = LinearMap.range (ϕ ∘ₗ Submodule.inclusion hNO)
                @[simp]
                theorem LinearMap.range_rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
                LinearMap.range f.rangeRestrict =
                theorem LinearMap.surjective_rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
                Function.Surjective f.rangeRestrict
                @[simp]
                theorem LinearMap.ker_rangeRestrict {R : Type u_1} {R₂ : Type u_2} {M : Type u_6} {M₂ : Type u_7} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) :
                LinearMap.ker f.rangeRestrict = LinearMap.ker f