Documentation

Mathlib.LinearAlgebra.Span.Basic

The span of a set of vectors, as a submodule #

Notations #

@[simp]
theorem Submodule.span_coe_eq_restrictScalars {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) [Semiring S] [SMul S R] [Module S M] [IsScalarTower S R M] :

A version of Submodule.span_eq for when the span is by a smaller ring.

theorem Submodule.image_span_subset {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :
f '' (span R s) N ms, f m N

A version of Submodule.map_span_le that does not require the RingHomSurjective assumption.

theorem Submodule.image_span_subset_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M) :
f '' (span R s) (span R₂ (f '' s))
theorem Submodule.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) :
map f (span R s) = span R₂ (f '' s)
theorem LinearMap.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) :

Alias of Submodule.map_span.

theorem Submodule.map_span_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :
map f (span R s) N ms, f m N
theorem LinearMap.map_span_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) (s : Set M) (N : Submodule R₂ M₂) :
Submodule.map f (Submodule.span R s) N ms, f m N

Alias of Submodule.map_span_le.

theorem Submodule.span_preimage_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M₂) :
span R (f ⁻¹' s) comap f (span R₂ s)

See also Submodule.span_preimage_eq.

theorem LinearMap.span_preimage_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] (f : F) (s : Set M₂) :

Alias of Submodule.span_preimage_le.


See also Submodule.span_preimage_eq.

theorem Submodule.mapsTo_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {s : Set M} {t : Set M₂} (h : Set.MapsTo (⇑f) s t) :
Set.MapsTo f (span R s) (span R₂ t)
theorem Set.MapsTo.submoduleSpan {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {f : F} {s : Set M} {t : Set M₂} (h : MapsTo (⇑f) s t) :
MapsTo f (Submodule.span R s) (Submodule.span R₂ t)

Alias of Submodule.mapsTo_span.

theorem Submodule.linearMap_eq_iff_of_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] {V : Submodule R M} (f g : V →ₗ[R] N) {S : Set M} (hV : V = span R S) :
f = g ∀ (s : S), f s, = g s,
theorem Submodule.linearMap_eq_iff_of_span_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (f g : M →ₗ[R] N) {S : Set M} (hM : span R S = ) :
f = g ∀ (s : S), f s = g s
theorem Submodule.linearMap_eq_zero_iff_of_span_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) {S : Set M} (hM : span R S = ) :
f = 0 ∀ (s : S), f s = 0
theorem Submodule.linearMap_eq_zero_iff_of_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {N : Type u_9} [AddCommMonoid N] [Module R N] {V : Submodule R M} (f : V →ₗ[R] N) {S : Set M} (hV : V = span R S) :
f = 0 ∀ (s : S), f s, = 0
theorem Submodule.span_smul_eq_of_isUnit {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) (hr : IsUnit r) :
span R (r s) = span R s

See Submodule.span_smul_eq (in RingTheory.Ideal.Operations) for span R (r • s) = r • span R s that holds for arbitrary r in a CommSemiring.

We can regard coe_iSup_of_chain as the statement that (↑) : (Submodule R M) → Set M is Scott continuous for the ω-complete partial order induced by the complete lattice structures.

def Submodule.inclusionSpan {R : Type u_1} {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) :
p →ₗ[R] (span S p)

The inclusion of an R-submodule into its S-span, as an R-linear map.

Equations
    Instances For
      @[simp]
      theorem Submodule.inclusionSpan_apply_coe {R : Type u_1} {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) (x : p) :
      ((inclusionSpan S p) x) = x
      theorem Submodule.injective_inclusionSpan {R : Type u_1} {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) :
      theorem Submodule.span_range_inclusionSpan {R : Type u_1} {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) :
      theorem Submodule.span_le_restrictScalars (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :

      If R is "smaller" ring than S then the span by R is smaller than the span by S.

      @[simp]
      theorem Submodule.span_subset_span (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :
      (span R s) (span S s)

      A version of Submodule.span_le_restrictScalars with coercions.

      @[simp]
      theorem Submodule.span_span_of_tower (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :
      span S (span R s) = span S s

      Taking the span by a large ring of the span by the small ring is the same as taking the span by just the large ring.

      theorem Submodule.span_eq_top_of_span_eq_top (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (s : Set M) (hs : span R s = ) :
      span S s =
      theorem Submodule.span_range_inclusion_eq_top {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] (p : Submodule R M) (q : Submodule S M) (h₁ : p restrictScalars R q) (h₂ : q span S p) :
      span S (Set.range (inclusion h₁)) =
      @[simp]
      theorem Submodule.span_range_inclusion_restrictScalars_eq_top (R : Type u_1) {M : Type u_4} (S : Type u_7) [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) [Semiring S] [SMul R S] [Module S M] [IsScalarTower R S M] :
      theorem Submodule.span_singleton_eq_span_singleton {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x y : M} :
      span R {x} = span R {y} ∃ (z : Rˣ), z x = y
      theorem Submodule.span_image {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} [RingHomSurjective σ₁₂] (f : F) :
      span R₂ (f '' s) = map f (span R s)
      @[simp]
      theorem Submodule.span_image' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {s : Set M} [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
      span R₂ (f '' s) = map f (span R s)
      theorem Submodule.apply_mem_span_image_of_mem_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M} (h : x span R s) :
      f x span R₂ (f '' s)
      theorem Submodule.apply_mem_span_image_iff_mem_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] {f : F} {x : M} {s : Set M} (hf : Function.Injective f) :
      f x span R₂ (f '' s) x span R s
      @[simp]
      theorem Submodule.map_subtype_span_singleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (x : p) :
      map p.subtype (span R {x}) = span R {x}
      theorem Submodule.notMem_span_of_apply_notMem_span_image {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M} (h : f xspan R₂ (f '' s)) :
      xspan R s

      f is an explicit argument so we can apply this theorem and obtain h as a new goal.

      @[deprecated Submodule.notMem_span_of_apply_notMem_span_image (since := "2025-05-23")]
      theorem Submodule.not_mem_span_of_apply_not_mem_span_image {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M} (h : f xspan R₂ (f '' s)) :
      xspan R s

      Alias of Submodule.notMem_span_of_apply_notMem_span_image.


      f is an explicit argument so we can apply this theorem and obtain h as a new goal.

      theorem Submodule.iSup_toAddSubmonoid {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ιSubmodule R M) :
      (⨆ (i : ι), p i).toAddSubmonoid = ⨆ (i : ι), (p i).toAddSubmonoid
      theorem Submodule.iSup_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ιSubmodule R M) {motive : MProp} {x : M} (hx : x ⨆ (i : ι), p i) (mem : ∀ (i : ι), xp i, motive x) (zero : motive 0) (add : ∀ (x y : M), motive xmotive ymotive (x + y)) :
      motive x

      An induction principle for elements of ⨆ i, p i. If C holds for 0 and all elements of p i for all i, and is preserved under addition, then it holds for all elements of the supremum of p.

      theorem Submodule.iSup_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ιSubmodule R M) {motive : (x : M) → x ⨆ (i : ι), p iProp} (mem : ∀ (i : ι) (x : M) (hx : x p i), motive x ) (zero : motive 0 ) (add : ∀ (x y : M) (hx : x ⨆ (i : ι), p i) (hy : y ⨆ (i : ι), p i), motive x hxmotive y hymotive (x + y) ) {x : M} (hx : x ⨆ (i : ι), p i) :
      motive x hx

      A dependent version of submodule.iSup_induction.

      The span of a finite subset is compact in the lattice of submodules.

      The span of a finite subset is compact in the lattice of submodules.

      def Submodule.prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') :
      Submodule R (M × M')

      The product of two submodules is a submodule.

      Equations
        Instances For
          @[simp]
          theorem Submodule.prod_coe {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') :
          (p.prod q₁) = p ×ˢ q₁
          @[simp]
          theorem Submodule.mem_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {p : Submodule R M} {q : Submodule R M'} {x : M × M'} :
          x p.prod q x.1 p x.2 q
          theorem Submodule.span_prod_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (s : Set M) (t : Set M') :
          span R (s ×ˢ t) (span R s).prod (span R t)
          @[simp]
          theorem Submodule.prod_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] :
          @[simp]
          theorem Submodule.prod_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] :
          theorem Submodule.prod_mono {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {M' : Type u_9} [AddCommMonoid M'] [Module R M'] {p p' : Submodule R M} {q q' : Submodule R M'} :
          p p'q q'p.prod q p'.prod q'
          @[simp]
          theorem Submodule.prod_inf_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ q₁' : Submodule R M') :
          p.prod q₁p'.prod q₁' = (pp').prod (q₁q₁')
          @[simp]
          theorem Submodule.prod_sup_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ q₁' : Submodule R M') :
          p.prod q₁p'.prod q₁' = (pp').prod (q₁q₁')
          theorem LinearMap.BilinMap.apply_apply_mem_of_mem_span {R : Type u_10} {M : Type u_11} {N : Type u_12} {P : Type u_13} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [AddCommMonoid P] [Module R M] [Module R N] [Module R P] (P' : Submodule R P) (s : Set M) (t : Set N) (B : M →ₗ[R] N →ₗ[R] P) (hB : xs, yt, (B x) y P') (x : M) (y : N) (hx : x Submodule.span R s) (hy : y Submodule.span R t) :
          (B x) y P'

          If a bilinear map takes values in a submodule along two sets, then the same is true along the span of these sets.

          @[simp]
          theorem Submodule.biSup_comap_subtype_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_10} (s : Set ι) (p : ιSubmodule R M) :
          is, comap (⨆ is, p i).subtype (p i) =
          theorem LinearMap.exists_ne_zero_of_sSup_eq {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {N : Submodule R M} {f : N →ₛₗ[σ₁₂] M₂} (h : f 0) (s : Set (Submodule R M)) (hs : sSup s = N) :
          ∃ (m : Submodule R M) (h : m s), f ∘ₛₗ Submodule.inclusion 0
          @[simp]
          theorem Submodule.span_neg {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (s : Set M) :
          span R (-s) = span R s
          theorem Submodule.isCompl_comap_subtype_of_isCompl_of_le {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {p q r : Submodule R M} (h₁ : IsCompl q r) (h₂ : q p) :
          theorem Submodule.comap_map_eq {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) (p : Submodule R M) :
          comap f (map f p) = pLinearMap.ker f
          theorem Submodule.comap_map_eq_self {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} (h : LinearMap.ker f p) :
          comap f (map f p) = p
          theorem Submodule.comap_map_sup_of_comap_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} {p : Submodule R M} {q : Submodule R₂ M₂} (le : comap f q p) :
          comap f (map f pq) = p
          theorem Submodule.isCoatom_comap_or_eq_top {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) {p : Submodule R₂ M₂} (hp : IsCoatom p) :
          theorem Submodule.isCoatom_comap_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Surjective f) {p : Submodule R₂ M₂} :
          theorem Submodule.isCoatom_map_of_ker_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Surjective f) {p : Submodule R M} (le : LinearMap.ker f p) (hp : IsCoatom p) :
          theorem Submodule.map_iInf_of_ker_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Surjective f) {ι : Sort u_9} {p : ιSubmodule R M} (h : LinearMap.ker f ⨅ (i : ι), p i) :
          map f (⨅ (i : ι), p i) = ⨅ (i : ι), map f (p i)
          theorem Submodule.comap_covBy_of_surjective {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : Function.Surjective f) {p q : Submodule R₂ M₂} (h : p q) :
          comap f p comap f q
          theorem LinearMap.range_domRestrict_eq_range_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
          range (f.domRestrict S) = range f Sker f =
          @[simp]
          theorem LinearMap.surjective_domRestrict_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} (hf : Function.Surjective f) :
          theorem Submodule.biSup_comap_eq_top_of_surjective {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {ι : Type u_9} (s : Set ι) (hs : s.Nonempty) (p : ιSubmodule R₂ M₂) (hp : is, p i = ) (f : M →ₛₗ[τ₁₂] M₂) (hf : Function.Surjective f) :
          is, comap f (p i) =
          theorem Submodule.biSup_comap_eq_top_of_range_eq_biSup {M : Type u_4} {M₂ : Type u_5} [AddCommGroup M] [AddCommGroup M₂] {R : Type u_9} {R₂ : Type u_10} [Semiring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] [Module R M] [Module R₂ M₂] {ι : Type u_11} (s : Set ι) (hs : s.Nonempty) (p : ιSubmodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = is, p i) :
          is, comap f (p i) =
          theorem Submodule.wcovBy_span_singleton_sup {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] (x : V) (s : Submodule K V) :
          s ⩿ span K {x}s

          There is no vector subspace between s and (K ∙ x) ⊔ s, WCovBy version.

          theorem Submodule.covBy_span_singleton_sup {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {x : V} {s : Submodule K V} (h : xs) :
          s span K {x}s

          There is no vector subspace between s and (K ∙ x) ⊔ s, CovBy version.

          theorem Submodule.disjoint_span_singleton {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {x : V} :
          Disjoint s (span K {x}) x sx = 0
          theorem Submodule.disjoint_span_singleton' {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {x : V} (x0 : x 0) :
          Disjoint s (span K {x}) xs
          theorem Submodule.disjoint_span_singleton_of_notMem {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {x : V} (hx : xs) :
          @[deprecated Submodule.disjoint_span_singleton_of_notMem (since := "2025-05-23")]
          theorem Submodule.disjoint_span_singleton_of_not_mem {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {x : V} (hx : xs) :

          Alias of Submodule.disjoint_span_singleton_of_notMem.

          theorem Submodule.isCompl_span_singleton_of_isCoatom_of_notMem {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {x : V} (hs : IsCoatom s) (hx : xs) :
          IsCompl s (span K {x})
          @[deprecated Submodule.isCompl_span_singleton_of_isCoatom_of_notMem (since := "2025-05-23")]
          theorem Submodule.isCompl_span_singleton_of_isCoatom_of_not_mem {K : Type u_3} {V : Type u_6} [DivisionRing K] [AddCommGroup V] [Module K V] {s : Submodule K V} {x : V} (hs : IsCoatom s) (hx : xs) :
          IsCompl s (span K {x})

          Alias of Submodule.isCompl_span_singleton_of_isCoatom_of_notMem.

          theorem LinearMap.map_le_map_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] (f : F) {p p' : Submodule R M} :
          theorem LinearMap.map_le_map_iff' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : ker f = ) {p p' : Submodule R M} :
          theorem LinearMap.map_injective {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : ker f = ) :
          theorem LinearMap.map_eq_top_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [Semiring R₂] [AddCommGroup M] [AddCommGroup M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {F : Type u_8} [FunLike F M M₂] [SemilinearMapClass F τ₁₂ M M₂] {f : F} (hf : range f = ) {p : Submodule R M} :
          Submodule.map f p = pker f =
          def LinearMap.toSpanSingleton (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :

          Given an element x of a module M over R, the natural map from R to scalar multiples of x. See also LinearMap.ringLmapEquivSelf.

          Equations
            Instances For
              @[simp]
              theorem LinearMap.toSpanSingleton_apply (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (b : R) :
              (toSpanSingleton R M x) b = b x
              theorem LinearMap.span_singleton_eq_range (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :

              The range of toSpanSingleton x is the span of x.

              theorem LinearMap.toSpanSingleton_one (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
              (toSpanSingleton R M x) 1 = x
              @[simp]
              theorem LinearMap.toSpanSingleton_zero (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] :
              theorem LinearMap.toSpanSingleton_eq_zero_iff (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
              toSpanSingleton R M x = 0 x = 0
              theorem LinearMap.submoduleOf_span_singleton_of_mem {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) {x : M} (hx : x N) :
              theorem LinearMap.eqOn_span_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F} :
              Set.EqOn f g (Submodule.span R s) Set.EqOn (⇑f) (⇑g) s

              Two linear maps are equal on Submodule.span s iff they are equal on s.

              theorem LinearMap.eqOn_span' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F} (H : Set.EqOn (⇑f) (⇑g) s) :
              Set.EqOn f g (Submodule.span R s)

              If two linear maps are equal on a set s, then they are equal on Submodule.span s.

              This version uses Set.EqOn, and the hidden argument will expand to h : x ∈ (span R s : Set M). See LinearMap.eqOn_span for a version that takes h : x ∈ span R s as an argument.

              theorem LinearMap.eqOn_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F} (H : Set.EqOn (⇑f) (⇑g) s) x : M (h : x Submodule.span R s) :
              f x = g x

              If two linear maps are equal on a set s, then they are equal on Submodule.span s.

              See also LinearMap.eqOn_span' for a version using Set.EqOn.

              theorem LinearMap.ext_on {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {s : Set M} {f g : F} (hv : Submodule.span R s = ) (h : Set.EqOn (⇑f) (⇑g) s) :
              f = g

              If s generates the whole module and linear maps f, g are equal on s, then they are equal.

              theorem LinearMap.ext_on_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [Semiring R₂] [AddCommMonoid M₂] [Module R₂ M₂] {F : Type u_8} {σ₁₂ : R →+* R₂} [FunLike F M M₂] [SemilinearMapClass F σ₁₂ M M₂] {ι : Sort u_9} {v : ιM} {f g : F} (hv : Submodule.span R (Set.range v) = ) (h : ∀ (i : ι), f (v i) = g (v i)) :
              f = g

              If the range of v : ι → M generates the whole module and linear maps f, g are equal at each v i, then they are equal.

              theorem LinearMap.ker_toSpanSingleton (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] {x : M} (h : x 0) :
              theorem LinearMap.span_singleton_sup_ker_eq_top {K : Type u_3} {V : Type u_6} [Field K] [AddCommGroup V] [Module K V] (f : V →ₗ[K] K) {x : V} (hx : f x 0) :
              noncomputable def LinearEquiv.toSpanNonzeroSingleton (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) :

              Given a nonzero element x of a torsion-free module M over a ring R, the natural isomorphism from R to the span of x given by $r \mapsto r \cdot x$.

              Equations
                Instances For
                  @[simp]
                  theorem LinearEquiv.toSpanNonzeroSingleton_apply (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) (t : R) :
                  (toSpanNonzeroSingleton R M x h) t = t x,
                  @[simp]
                  theorem LinearEquiv.toSpanNonzeroSingleton_symm_apply_smul (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) (m : (Submodule.span R {x})) :
                  (toSpanNonzeroSingleton R M x h).symm m x = m
                  theorem LinearEquiv.toSpanNonzeroSingleton_one (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) :
                  (toSpanNonzeroSingleton R M x h) 1 = x,
                  @[reducible, inline]
                  noncomputable abbrev LinearEquiv.coord (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) :

                  Given a nonzero element x of a torsion-free module M over a ring R, the natural isomorphism from the span of x to R given by $r \cdot x \mapsto r$.

                  Equations
                    Instances For
                      theorem LinearEquiv.coord_self (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) :
                      (coord R M x h) x, = 1
                      theorem LinearEquiv.coord_apply_smul (R : Type u_1) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M] (x : M) (h : x 0) (y : (Submodule.span R {x})) :
                      (coord R M x h) y x = y