Documentation

Mathlib.LinearAlgebra.Span

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

Notations #

def Submodule.span (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :

The span of a set s ⊆ M is the smallest submodule of M that contains s.

Equations
Instances For
    theorem Submodule.isPrincipal_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) :
    Submodule.IsPrincipal S ∃ (a : M), S = Submodule.span R {a}
    class Submodule.IsPrincipal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) :

    An R-submodule of M is principal if it is generated by one element.

    Instances
      theorem Submodule.IsPrincipal.principal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) [Submodule.IsPrincipal S] :
      ∃ (a : M), S = Submodule.span R {a}
      theorem Submodule.mem_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} :
      x Submodule.span R s ∀ (p : Submodule R M), s px p
      theorem Submodule.subset_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      s (Submodule.span R s)
      theorem Submodule.span_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : Submodule R M} :
      Submodule.span R s p s p
      theorem Submodule.span_mono {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {t : Set M} (h : s t) :
      theorem Submodule.span_eq_of_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} (h₁ : s p) (h₂ : p Submodule.span R s) :
      theorem Submodule.span_eq {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
      Submodule.span R p = p
      theorem Submodule.span_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {t : Set M} (hs : s (Submodule.span R t)) (ht : t (Submodule.span R s)) :
      @[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 '' (Submodule.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 '' (Submodule.span R s) (Submodule.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) :
      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₂) :
      Submodule.map f (Submodule.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.

      @[simp]
      theorem Submodule.span_insert_zero {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      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₂) :
      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.

      theorem Submodule.closure_subset_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      theorem Submodule.closure_le_toAddSubmonoid_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      AddSubmonoid.closure s (Submodule.span R s).toAddSubmonoid
      @[simp]
      theorem Submodule.span_closure {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      theorem Submodule.span_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {p : MProp} (h : x Submodule.span R s) (mem : xs, p x) (zero : p 0) (add : ∀ (x y : M), p xp yp (x + y)) (smul : ∀ (a : R) (x : M), p xp (a x)) :
      p x

      An induction principle for span membership. If p holds for 0 and all elements of s, and is preserved under addition and scalar multiplication, then p holds for all elements of the span of s.

      theorem Submodule.span_induction₂ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : MMProp} {a : M} {b : M} (ha : a Submodule.span R s) (hb : b Submodule.span R s) (mem_mem : xs, ys, p x y) (zero_left : ∀ (y : M), p 0 y) (zero_right : ∀ (x : M), p x 0) (add_left : ∀ (x₁ x₂ y : M), p x₁ yp x₂ yp (x₁ + x₂) y) (add_right : ∀ (x y₁ y₂ : M), p x y₁p x y₂p x (y₁ + y₂)) (smul_left : ∀ (r : R) (x y : M), p x yp (r x) y) (smul_right : ∀ (r : R) (x y : M), p x yp x (r y)) :
      p a b

      An induction principle for span membership. This is a version of Submodule.span_induction for binary predicates.

      theorem Submodule.span_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x Submodule.span R sProp} (mem : ∀ (x : M) (h : x s), p x ) (zero : p 0 ) (add : ∀ (x : M) (hx : x Submodule.span R s) (y : M) (hy : y Submodule.span R s), p x hxp y hyp (x + y) ) (smul : ∀ (a : R) (x : M) (hx : x Submodule.span R s), p x hxp (a x) ) {x : M} (hx : x Submodule.span R s) :
      p x hx

      A dependent version of Submodule.span_induction.

      theorem Submodule.span_eq_closure {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      (Submodule.span R s).toAddSubmonoid = AddSubmonoid.closure (Set.univ s)
      theorem Submodule.closure_induction {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {p : MProp} (h : x Submodule.span R s) (zero : p 0) (add : ∀ (x y : M), p xp yp (x + y)) (smul_mem : ∀ (r : R), xs, p (r x)) :
      p x

      A variant of span_induction that combines ∀ x ∈ s, p x and ∀ r x, p x → p (r • x) into a single condition ∀ r, ∀ x ∈ s, p (r • x), which can be easier to verify.

      theorem Submodule.closure_induction' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} {p : (x : M) → x Submodule.span R sProp} (zero : p 0 ) (add : ∀ (x : M) (hx : x Submodule.span R s) (y : M) (hy : y Submodule.span R s), p x hxp y hyp (x + y) ) (smul_mem : ∀ (r : R) (x : M) (h : x s), p (r x) ) {x : M} (hx : x Submodule.span R s) :
      p x hx

      A dependent version of Submodule.closure_induction.

      @[simp]
      theorem Submodule.span_span_coe_preimage {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      Submodule.span R (Subtype.val ⁻¹' s) =
      @[simp]
      theorem Submodule.span_setOf_mem_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
      Submodule.span R {x : (Submodule.span R s) | x s} =
      @[simp]
      theorem Submodule.span_nat_eq {M : Type u_4} [AddCommMonoid M] (s : AddSubmonoid M) :
      (Submodule.span s).toAddSubmonoid = s
      def Submodule.gi (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] :

      span forms a Galois insertion with the coercion from submodule to set.

      Equations
      Instances For
        @[simp]
        theorem Submodule.span_empty {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
        @[simp]
        theorem Submodule.span_univ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
        Submodule.span R Set.univ =
        theorem Submodule.span_union {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (t : Set M) :
        theorem Submodule.span_iUnion {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (s : ιSet M) :
        Submodule.span R (⋃ (i : ι), s i) = ⨆ (i : ι), Submodule.span R (s i)
        theorem Submodule.span_iUnion₂ {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_10} {κ : ιSort u_9} (s : (i : ι) → κ iSet M) :
        Submodule.span R (⋃ (i : ι), ⋃ (j : κ i), s i j) = ⨆ (i : ι), ⨆ (j : κ i), Submodule.span R (s i j)
        theorem Submodule.span_attach_biUnion {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [DecidableEq M] {α : Type u_9} (s : Finset α) (f : { x : α // x s }Finset M) :
        Submodule.span R (Finset.biUnion (Finset.attach s) f) = ⨆ (x : { x : α // x s }), Submodule.span R (f x)
        theorem Submodule.sup_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} :
        theorem Submodule.span_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {s : Set M} :
        theorem Submodule.span_eq_iSup_of_singleton_spans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) :
        Submodule.span R s = ⨆ x ∈ s, Submodule.span R {x}
        theorem Submodule.span_range_eq_iSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_9} {v : ιM} :
        Submodule.span R (Set.range v) = ⨆ (i : ι), Submodule.span R {v i}
        theorem Submodule.span_smul_le {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) (r : R) :
        theorem Submodule.subset_span_trans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {U : Set M} {V : Set M} {W : Set M} (hUV : U (Submodule.span R V)) (hVW : V (Submodule.span R W)) :
        U (Submodule.span R W)
        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) :

        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.

        @[simp]
        theorem Submodule.coe_iSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} [Nonempty ι] (S : ιSubmodule R M) (H : Directed (fun (x x_1 : Submodule R M) => x x_1) S) :
        (iSup S) = ⋃ (i : ι), (S i)
        @[simp]
        theorem Submodule.mem_iSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} [Nonempty ι] (S : ιSubmodule R M) (H : Directed (fun (x x_1 : Submodule R M) => x x_1) S) {x : M} :
        x iSup S ∃ (i : ι), x S i
        theorem Submodule.mem_sSup_of_directed {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Submodule R M)} {z : M} (hs : Set.Nonempty s) (hdir : DirectedOn (fun (x x_1 : Submodule R M) => x x_1) s) :
        z sSup s ∃ y ∈ s, z y
        @[simp]
        theorem Submodule.coe_iSup_of_chain {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (a : →o Submodule R M) :
        (⨆ (k : ), a k) = ⋃ (k : ), (a k)

        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.

        @[simp]
        theorem Submodule.mem_iSup_of_chain {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (a : →o Submodule R M) (m : M) :
        m ⨆ (k : ), a k ∃ (k : ), m a k
        theorem Submodule.mem_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {p : Submodule R M} {p' : Submodule R M} :
        x p p' ∃ y ∈ p, ∃ z ∈ p', y + z = x
        theorem Submodule.mem_sup' {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {p : Submodule R M} {p' : Submodule R M} :
        x p p' ∃ (y : p) (z : p'), y + z = x
        theorem Submodule.exists_add_eq_of_codisjoint {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} {p' : Submodule R M} (h : Codisjoint p p') (x : M) :
        ∃ y ∈ p, ∃ z ∈ p', y + z = x
        theorem Submodule.coe_sup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
        (p p') = p + p'
        theorem Submodule.sup_toAddSubmonoid {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
        (p p').toAddSubmonoid = p.toAddSubmonoid p'.toAddSubmonoid
        theorem Submodule.mem_span_singleton_self {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
        theorem Submodule.nontrivial_span_singleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} (h : x 0) :
        theorem Submodule.mem_span_singleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {y : M} :
        x Submodule.span R {y} ∃ (a : R), a y = x
        theorem Submodule.le_span_singleton_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Submodule R M} {v₀ : M} :
        s Submodule.span R {v₀} vs, ∃ (r : R), r v₀ = v
        theorem Submodule.span_singleton_eq_top_iff (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) :
        Submodule.span R {x} = ∀ (v : M), ∃ (r : R), r x = v
        @[simp]
        theorem Submodule.span_zero_singleton (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
        theorem Submodule.span_singleton_eq_range (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (y : M) :
        (Submodule.span R {y}) = Set.range fun (x : R) => x y
        theorem Submodule.span_singleton_smul_le (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_9} [Monoid S] [SMul S R] [MulAction S M] [IsScalarTower S R M] (r : S) (x : M) :
        theorem Submodule.span_singleton_group_smul_eq (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {G : Type u_9} [Group G] [SMul G R] [MulAction G M] [IsScalarTower G R M] (g : G) (x : M) :
        theorem Submodule.span_singleton_smul_eq {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {r : R} (hr : IsUnit r) (x : M) :
        theorem Submodule.disjoint_span_singleton {K : Type u_9} {E : Type u_10} [DivisionRing K] [AddCommGroup E] [Module K E] {s : Submodule K E} {x : E} :
        Disjoint s (Submodule.span K {x}) x sx = 0
        theorem Submodule.disjoint_span_singleton' {K : Type u_9} {E : Type u_10} [DivisionRing K] [AddCommGroup E] [Module K E] {p : Submodule K E} {x : E} (x0 : x 0) :
        Disjoint p (Submodule.span K {x}) xp
        theorem Submodule.mem_span_singleton_trans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {y : M} {z : M} (hxy : x Submodule.span R {y}) (hyz : y Submodule.span R {z}) :
        theorem Submodule.span_insert {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (s : Set M) :
        theorem Submodule.span_insert_eq_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} (h : x Submodule.span R s) :
        theorem Submodule.span_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
        theorem Submodule.mem_span_insert {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {s : Set M} {y : M} :
        x Submodule.span R (insert y s) ∃ (a : R), ∃ z ∈ Submodule.span R s, x = a y + z
        theorem Submodule.mem_span_pair {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} {y : M} {z : M} :
        z Submodule.span R {x, y} ∃ (a : R) (b : R), a x + b y = z
        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] :

        A version of Submodule.span_le_restrictScalars with coercions.

        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] :

        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_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} :
        Submodule.span R s = xs, x = 0
        @[simp]
        theorem Submodule.span_singleton_eq_bot {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {x : M} :
        @[simp]
        theorem Submodule.span_zero {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] :
        @[simp]
        theorem Submodule.span_singleton_le_iff_mem {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (m : M) (p : Submodule R 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 : M} {y : M} :
        Submodule.span R {x} = Submodule.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) :
        @[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₂) :
        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 Submodule.span R s) :
        f x Submodule.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 Submodule.span R₂ (f '' s) x Submodule.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) :
        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 xSubmodule.span R₂ (f '' s)) :
        xSubmodule.span R s

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

        theorem Submodule.iSup_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ιSet M) :
        ⨆ (i : ι), Submodule.span R (p i) = Submodule.span R (⋃ (i : ι), p i)
        theorem Submodule.iSup_eq_span {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 = Submodule.span R (⋃ (i : ι), (p i))
        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) {C : MProp} {x : M} (hx : x ⨆ (i : ι), p i) (hp : ∀ (i : ι), xp i, C x) (h0 : C 0) (hadd : ∀ (x y : M), C xC yC (x + y)) :
        C 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) {C : (x : M) → x ⨆ (i : ι), p iProp} (mem : ∀ (i : ι) (x : M) (hx : x p i), C x ) (zero : C 0 ) (add : ∀ (x y : M) (hx : x ⨆ (i : ι), p i) (hy : y ⨆ (i : ι), p i), C x hxC y hyC (x + y) ) {x : M} (hx : x ⨆ (i : ι), p i) :
        C 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.

        theorem Submodule.submodule_eq_sSup_le_nonzero_spans {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) :
        p = sSup {T : Submodule R M | ∃ m ∈ p, m 0 T = Submodule.span R {m}}

        A submodule is equal to the supremum of the spans of the submodule's nonzero elements.

        theorem Submodule.lt_sup_iff_not_mem {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {I : Submodule R M} {a : M} :
        I < I Submodule.span R {a} aI
        theorem Submodule.mem_iSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Sort u_9} (p : ιSubmodule R M) {m : M} :
        m ⨆ (i : ι), p i ∀ (N : Submodule R M), (∀ (i : ι), p i N)m N
        theorem Submodule.mem_sSup {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set (Submodule R M)} {m : M} :
        m sSup s ∀ (N : Submodule R M), (ps, p N)m N
        theorem Submodule.mem_span_finite_of_mem_span {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Set M} {x : M} (hx : x Submodule.span R S) :
        ∃ (T : Finset M), T S x Submodule.span R T

        For every element in the span of a set, there exists a finite subset of the set such that the element is contained in the span of the subset.

        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
        • One or more equations did not get rendered due to their size.
        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') :
          (Submodule.prod p 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 Submodule.prod p 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') :
          @[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 : Submodule R M} {p' : Submodule R M} {q : Submodule R M'} {q' : Submodule R M'} :
          p p'q q'Submodule.prod p q Submodule.prod p' q'
          @[simp]
          theorem Submodule.prod_inf_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') (q₁' : Submodule R M') :
          Submodule.prod p q₁ Submodule.prod p' q₁' = Submodule.prod (p p') (q₁ q₁')
          @[simp]
          theorem Submodule.prod_sup_prod {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) (p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') (q₁' : Submodule R M') :
          Submodule.prod p q₁ Submodule.prod p' q₁' = Submodule.prod (p p') (q₁ q₁')
          @[simp]
          theorem Submodule.span_neg {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] (s : Set M) :
          theorem Submodule.mem_span_insert' {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {x : M} {y : M} {s : Set M} :
          x Submodule.span R (insert y s) ∃ (a : R), x + a y Submodule.span R s
          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) :
          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) :
          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} :
          @[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) :
          @[simp]
          theorem Submodule.biSup_comap_subtype_eq_top {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommGroup M] [Module R M] {ι : Type u_9} (s : Set ι) (p : ιSubmodule R M) :
          ⨆ i ∈ s, Submodule.comap (Submodule.subtype (⨆ i ∈ s, p i)) (p i) =
          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 : Set.Nonempty s) (p : ιSubmodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ) (f : M →ₛₗ[τ₁₂] M₂) (hf : Function.Surjective f) :
          ⨆ i ∈ s, Submodule.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} [Ring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] [Module R M] [Module R₂ M₂] {ι : Type u_11} (s : Set ι) (hs : Set.Nonempty s) (p : ιSubmodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
          ⨆ i ∈ s, Submodule.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) (p : Submodule K V) :

          There is no vector subspace between p and (K ∙ x) ⊔ p, 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} {p : Submodule K V} (h : xp) :

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

          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 : Submodule R M} {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 : LinearMap.ker f = ) {p : Submodule R M} {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 : LinearMap.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 : LinearMap.range f = ) {p : Submodule R M} :
          @[simp]
          theorem LinearMap.toSpanSingleton_apply (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) (b : R) :
          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

            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) :
            @[simp]
            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 : 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 : 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 : 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 : 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₂] {ι : Type u_9} {v : ιM} {f : 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) :
            R ≃ₗ[R] (Submodule.span R {x})

            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
            • One or more equations did not get rendered due to their size.
            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) :
              (LinearEquiv.toSpanNonzeroSingleton R M x h) t = { val := t x, property := }
              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) :
              (LinearEquiv.toSpanNonzeroSingleton R M x h) 1 = { val := x, property := }
              @[inline, reducible]
              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) :
              (Submodule.span R {x}) ≃ₗ[R] R

              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) :
                (LinearEquiv.coord R M x h) { val := x, property := } = 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})) :
                (LinearEquiv.coord R M x h) y x = y