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) :
    S.IsPrincipal ∃ (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} :
      ∀ {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M} {S : Submodule R M} [self : S.IsPrincipal], ∃ (a : M), S = Submodule.span R {a}
      theorem Submodule.IsPrincipal.principal {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) [S.IsPrincipal] :
      ∃ (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)) :
      theorem Submodule.coe_span_eq_self {R : Type u_1} {M : Type u_4} {S : Type u_7} [Semiring R] [AddCommMonoid M] [Module R M] [SetLike S M] [AddSubmonoidClass S M] [SMulMemClass S R M] (s : S) :
      (Submodule.span R s) = s

      A version of Submodule.span_eq for subobjects closed under addition and scalar multiplication and containing zero. In general, this should not be used directly, but can be used to quickly generate proofs for specific types of subobjects.

      @[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] {s : Set M} {p : (x : M) → x Submodule.span R sProp} (mem : ∀ (x : M) (h : x s), p x ) (zero : p 0 ) (add : ∀ (x y : M) (hx : x Submodule.span R s) (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

      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.

      @[deprecated Submodule.span_induction]
      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 y : M) (hx : x Submodule.span R s) (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

      Alias of Submodule.span_induction.


      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 : (x y : M) → x Submodule.span R sy Submodule.span R sProp} (mem_mem : ∀ (x y : M) (hx : x s) (hy : y s), p x y ) (zero_left : ∀ (y : M) (hy : y Submodule.span R s), p 0 y hy) (zero_right : ∀ (x : M) (hx : x Submodule.span R s), p x 0 hx ) (add_left : ∀ (x y z : M) (hx : x Submodule.span R s) (hy : y Submodule.span R s) (hz : z Submodule.span R s), p x z hx hzp y z hy hzp (x + y) z hz) (add_right : ∀ (x y z : M) (hx : x Submodule.span R s) (hy : y Submodule.span R s) (hz : z Submodule.span R s), p x y hx hyp x z hx hzp x (y + z) hx ) (smul_left : ∀ (r : R) (x y : M) (hx : x Submodule.span R s) (hy : y Submodule.span R s), p x y hx hyp (r x) y hy) (smul_right : ∀ (r : R) (x y : M) (hx : x Submodule.span R s) (hy : y Submodule.span R s), p x y hx hyp x (r y) hx ) {a : M} {b : M} (ha : a Submodule.span R s) (hb : b Submodule.span R s) :
      p a b ha hb

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

      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] {s : Set M} {p : (x : M) → x Submodule.span R sProp} (zero : p 0 ) (add : ∀ (x y : M) (hx : x Submodule.span R s) (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 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.

      @[deprecated Submodule.closure_induction]
      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 y : M) (hx : x Submodule.span R s) (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

      Alias of Submodule.closure_induction.


      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.

      @[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
      @[simp]
      theorem Submodule.span_int_eq {M : Type u_9} [AddCommGroup M] (s : AddSubgroup M) :
      (Submodule.span s).toAddSubgroup = 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 (s.attach.biUnion 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 = xs, 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] {ι : Sort 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 (x1 x2 : Submodule R M) => x1 x2) 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 (x1 x2 : Submodule R M) => x1 x2) 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 : s.Nonempty) (hdir : DirectedOn (fun (x1 x2 : Submodule R M) => x1 x2) s) :
        z sSup s ys, 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' yp, zp', 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) :
        yp, zp', 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.sup_toAddSubgroup {R : Type u_9} {M : Type u_10} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M) (p' : Submodule R M) :
        (p p').toAddSubgroup = p.toAddSubgroup p'.toAddSubgroup
        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), zSubmodule.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) :
        Submodule.map p.subtype (Submodule.span R {x}) = Submodule.span R {x}
        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.

        Equations
        • =
        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 | mp, 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
        • p.prod q₁ = { carrier := p ×ˢ q₁, add_mem' := , zero_mem' := , smul_mem' := }
        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') :
          @[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'] :
          .prod =
          @[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'] :
          .prod =
          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'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 : Submodule R M) (p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') (q₁' : Submodule R M') :
          p.prod q₁ p'.prod q₁' = (p p').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 : Submodule R M) (p' : Submodule R M) {M' : Type u_9} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') (q₁' : Submodule R M') :
          p.prod q₁ p'.prod q₁' = (p p').prod (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
          instance Submodule.instIsModularLattice {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] :
          Equations
          • =
          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 : Submodule R M} {q : Submodule R M} {r : Submodule R M} (h₁ : IsCompl q r) (h₂ : q p) :
          IsCompl (Submodule.comap p.subtype q) (Submodule.comap p.subtype r)
          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) :
          Function.Surjective (f.domRestrict S) S LinearMap.ker 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) :
          is, Submodule.comap (⨆ is, p i).subtype (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 : s.Nonempty) (p : ιSubmodule R₂ M₂) (hp : is, p i = ) (f : M →ₛₗ[τ₁₂] M₂) (hf : Function.Surjective f) :
          is, 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 : s.Nonempty) (p : ιSubmodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = is, p i) :
          is, 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₂] {ι : Sort 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 = t x,
              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 = 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) :
              (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) 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})) :
                (LinearEquiv.coord R M x h) y x = y