The span of a set of vectors, as a submodule

• Submodule.span s is defined to be the smallest submodule containing the set s.

Notation

• We introduce the notation R ∙ v for the span of a singleton, Submodule.span R {v}. This is \span, not the same as the scalar multiplication •/\bub.

theorem AddSubmonoid.toNatSubmodule_closure {M : Type u_4} [AddCommMonoid M] (s : Set M) : toNatSubmodule (closure s) = Submodule.span ℕ 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] : span S ↑p = restrictScalars S p

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 : M →ₛₗ[σ₁₂] M₂) (s : Set M) (N : Submodule R₂ M₂) : ⇑f '' ↑(span R s) ⊆ ↑N ↔ ∀ m ∈ s, 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 : M →ₛₗ[σ₁₂] M₂) (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₂] [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (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₂] [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M) : Submodule.map f (Submodule.span R s) = Submodule.span R₂ (⇑f '' s)

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₂] [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M) (N : Submodule R₂ M₂) : map f (span R s) ≤ N ↔ ∀ m ∈ s, 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₂] [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : Set M) (N : Submodule R₂ M₂) : Submodule.map f (Submodule.span R s) ≤ N ↔ ∀ m ∈ s, 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 : M →ₛₗ[σ₁₂] M₂) (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 : M →ₛₗ[σ₁₂] M₂) (s : Set M₂) : Submodule.span R (⇑f ⁻¹' s) ≤ Submodule.comap f (Submodule.span R₂ s)

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 : M →ₛₗ[σ₁₂] M₂} {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 : M →ₛₗ[σ₁₂] M₂} {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_8} [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_8} [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_8} [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_8} [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.

theorem Submodule.coe_scott_continuous {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : OmegaCompletePartialOrder.ωScottContinuous SetLike.coe

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.

@[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) : Function.Injective ⇑(inclusionSpan S p)

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) : span S (Set.range ⇑(inclusionSpan S p)) = ⊤

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] : span R s ≤ restrictScalars R (span S s)

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] : span S (Set.range ⇑(inclusion ⋯)) = ⊤

theorem Submodule.span_singleton_eq_span_singleton {R : Type u_8} {M : Type u_9} [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] {x y : M} : R ∙ x = R ∙ y ↔ ∃ (z : Rˣ), z • x = y

@[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)

@[simp]

theorem Submodule.span_image_linearEquiv {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} {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (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₂] [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {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₂] [RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂} {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 (R ∙ x) = 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₂] [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : Set M} (h : f x ∉ span R₂ (⇑f '' s)) : x ∉ span R s

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_8} (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_8} (p : ι → Submodule R M) {motive : M → Prop} {x : M} (hx : x ∈ ⨆ (i : ι), p i) (mem : ∀ (i : ι), ∀ x ∈ p i, motive x) (zero : motive 0) (add : ∀ (x y : M), motive x → motive y → motive (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_8} (p : ι → Submodule R M) {motive : (x : M) → x ∈ ⨆ (i : ι), p i → Prop} (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 hx → motive y hy → motive (x + y) ⋯) {x : M} (hx : x ∈ ⨆ (i : ι), p i) : motive x hx

A dependent version of submodule.iSup_induction.

theorem Submodule.singleton_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : IsCompactElement (R ∙ x)

theorem Submodule.finset_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Finset M) : IsCompactElement (span R ↑S)

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

theorem Submodule.finite_span_isCompactElement {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (S : Set M) (h : S.Finite) : IsCompactElement (span R S)

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

instance Submodule.instIsCompactlyGenerated {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] : IsCompactlyGenerated (Submodule R M)

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_8} [AddCommMonoid M'] [Module R M'] (q₁ : Submodule R M') : Submodule R (M × M')

The product of two submodules is a submodule.

@[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_8} [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_8} [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_8} [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_8} [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_8} [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_8} [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_8} [AddCommMonoid M'] [Module R M'] (q₁ 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 p' : Submodule R M) {M' : Type u_8} [AddCommMonoid M'] [Module R M'] (q₁ q₁' : Submodule R M') : p.prod q₁ ⊔ p'.prod q₁' = (p ⊔ p').prod (q₁ ⊔ q₁')

theorem LinearMap.BilinMap.apply_apply_mem_of_mem_span {R : Type u_9} {M : Type u_10} {N : Type u_11} {P : Type u_12} [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 : ∀ x ∈ s, ∀ y ∈ t, (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_9} (s : Set ι) (p : ι → Submodule R M) : ⨆ i ∈ s, comap (⨆ i ∈ s, 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

theorem Submodule.span_range_subtype_eq_top_iff {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_9} (p : Submodule R M) {s : ι → M} (hs : ∀ (i : ι), s i ∈ p) : span R (Set.range fun (i : ι) => ⟨s i, ⋯⟩) = ⊤ ↔ span R (Set.range s) = p

theorem Submodule.comap_le_comap_iff_of_le_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₂] {σ₁₂ : R →+* R₂} [AddCommMonoid M₂] [Module R₂ M₂] {f : M →ₛₗ[σ₁₂] M₂} [RingHomSurjective σ₁₂] {p q : Submodule R₂ M₂} (hp : p ≤ f.range) : comap f p ≤ comap f q ↔ p ≤ q

theorem Submodule.comap_sup_of_injective {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 : M →ₛₗ[σ₁₂] M₂} [RingHomSurjective σ₁₂] {p q : Submodule R₂ M₂} (hf : Function.Injective ⇑f) (hp : p ≤ f.range) (hq : q ≤ f.range) : comap f (p ⊔ q) = comap f p ⊔ comap f q

theorem AddSubgroup.toIntSubmodule_closure {M : Type u_4} [AddCommGroup M] (s : Set M) : toIntSubmodule (closure s) = Submodule.span ℤ s

@[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

instance Submodule.instIsModularLattice {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] : IsModularLattice (Submodule R M)

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) : IsCompl (comap p.subtype q) (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 : M →ₛₗ[τ₁₂] M₂) (p : Submodule R M) : comap f (map f p) = p ⊔ f.ker

theorem Submodule.map_lt_map_of_le_of_sup_lt_sup {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 τ₁₂] {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} (hab : p ≤ p') (h : p ⊔ f.ker < p' ⊔ f.ker) : map f p < map f p'

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 : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} (h : f.ker ≤ 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 : M →ₛₗ[τ₁₂] M₂} {p : Submodule R M} {q : Submodule R₂ M₂} (le : comap f q ≤ p) : comap f (map f p ⊔ q) = 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 : M →ₛₗ[τ₁₂] M₂) {p : Submodule R₂ M₂} (hp : IsCoatom p) : IsCoatom (comap f p) ∨ comap f 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 : M →ₛₗ[τ₁₂] M₂} (hf : Function.Surjective ⇑f) {p : Submodule R₂ M₂} : IsCoatom (comap f p) ↔ IsCoatom p

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 : M →ₛₗ[τ₁₂] M₂} (hf : Function.Surjective ⇑f) {p : Submodule R M} (le : f.ker ≤ p) (hp : IsCoatom p) : IsCoatom (map f 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 : M →ₛₗ[τ₁₂] M₂} (hf : Function.Surjective ⇑f) {ι : Sort u_8} {p : ι → Submodule R M} (h : f.ker ≤ ⨅ (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 : M →ₛₗ[τ₁₂] M₂} (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} : (f.domRestrict S).range = f.range ↔ S ⊔ f.ker = ⊤

@[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 ⊔ f.ker = ⊤

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_8} (s : Set ι) (hs : s.Nonempty) (p : ι → Submodule R₂ M₂) (hp : ⨆ i ∈ s, p i = ⊤) (f : M →ₛₗ[τ₁₂] M₂) (hf : Function.Surjective ⇑f) : ⨆ i ∈ s, 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_8} {R₂ : Type u_9} [Semiring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] [Module R M] [Module R₂ M₂] {ι : Type u_10} (s : Set ι) (hs : s.Nonempty) (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : f.range = ⨆ i ∈ s, p i) : ⨆ i ∈ s, comap f (p i) = ⊤

theorem Submodule.map_strict_mono_or_ker_sup_lt_ker_sup {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Ring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {p p' : Submodule R M} (f : M →ₛₗ[τ₁₂] M₂) (hab : p < p') : map f p < map f p' ∨ f.ker ⊓ p < f.ker ⊓ p'

theorem LinearMap.ker_inf_lt_ker_inf_of_map_eq_of_lt {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Ring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} (hab : p < p') (q : Submodule.map f p = Submodule.map f p') : f.ker ⊓ p < f.ker ⊓ p'

theorem Submodule.map_strict_mono_of_ker_inf_eq {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [Ring R] [Semiring R₂] [AddCommGroup M] [Module R M] [AddCommGroup M₂] [Module R₂ M₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂] {p p' : Submodule R M} {f : M →ₛₗ[τ₁₂] M₂} (hab : p < p') (q : f.ker ⊓ p = f.ker ⊓ p') : map f p < map f p'

theorem Submodule.disjoint_span_singleton'' {R : Type u_1} {M : Type u_4} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {x : M} : Disjoint s (R ∙ x) ↔ ∀ (r : R), r • x ∈ s → r • x = 0

Version of disjoint_span_singleton that works when the scalars are not a field.

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 ⩿ 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 : x ∉ s) : s ⋖ 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 (K ∙ x) ↔ x ∈ s → x = 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} (hx : x ≠ 0) : Disjoint s (K ∙ x) ↔ x ∉ s

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 : x ∉ s) : Disjoint s (K ∙ x)

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 : x ∉ s) : IsCompl s (K ∙ x)

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 : M →ₛₗ[τ₁₂] M₂) {p p' : Submodule R M} : Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p' ⊔ f.ker

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 : M →ₛₗ[τ₁₂] M₂} (hf : f.ker = ⊥) {p p' : Submodule R M} : Submodule.map f p ≤ Submodule.map f p' ↔ p ≤ p'

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 : M →ₛₗ[τ₁₂] M₂} (hf : f.ker = ⊥) : Function.Injective (Submodule.map 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 : M →ₛₗ[τ₁₂] M₂} (hf : f.range = ⊤) {p : Submodule R M} : Submodule.map f p = ⊤ ↔ p ⊔ f.ker = ⊤

def LinearMap.toSpanSingleton (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : R →ₗ[R] 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.

@[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.smulRight_id (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : id.smulRight = toSpanSingleton R M

theorem LinearMap.toSpanSingleton_apply_one (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : (toSpanSingleton R M x) 1 = x

@[deprecated LinearMap.toSpanSingleton_apply_one (since := "2025-12-05")]

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

Alias of LinearMap.toSpanSingleton_apply_one.

theorem LinearMap.toSpanSingleton_injective (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : Function.Injective (toSpanSingleton R M)

@[simp]

theorem LinearMap.toSpanSingleton_zero (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] : toSpanSingleton R M 0 = 0

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.toSpanSingleton_add {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x y : M) : toSpanSingleton R M (x + y) = toSpanSingleton R M x + toSpanSingleton R M y

theorem LinearMap.toSpanSingleton_smul {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] {S : Type u_8} [Monoid S] [DistribMulAction S M] [SMulCommClass R S M] (r : S) (x : M) : toSpanSingleton R M (r • x) = r • toSpanSingleton R M x

theorem LinearMap.toSpanSingleton_isIdempotentElem_iff {R : Type u_1} [Semiring R] {e : R} : IsIdempotentElem (toSpanSingleton R R e) ↔ IsIdempotentElem e

theorem LinearMap.isIdempotentElem_map_one_iff {R : Type u_1} [Semiring R] {f : Module.End R R} : IsIdempotentElem (f 1) ↔ IsIdempotentElem f

@[deprecated LinearMap.isIdempotentElem_map_one_iff (since := "2025-12-05")]

theorem LinearMap.isIdempotentElem_apply_one_iff {R : Type u_1} [Semiring R] {f : Module.End R R} : IsIdempotentElem (f 1) ↔ IsIdempotentElem f

Alias of LinearMap.isIdempotentElem_map_one_iff.

theorem LinearMap.range_toSpanSingleton {R : Type u_1} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : (toSpanSingleton R M x).range = R ∙ x

The range of toSpanSingleton x is the span of x.

theorem LinearMap.span_singleton_eq_range (R : Type u_1) (M : Type u_4) [Semiring R] [AddCommMonoid M] [Module R M] (x : M) : R ∙ x = (toSpanSingleton R M x).range

theorem LinearMap.comp_toSpanSingleton {R : Type u_1} {M : Type u_4} {M₂ : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] (f : M →ₗ[R] M₂) (x : M) : f ∘ₗ toSpanSingleton R M x = toSpanSingleton R M₂ (f x)

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) : (R ∙ x).submoduleOf N = R ∙ ⟨x, hx⟩

@[simp]

theorem LinearMap.ker_toSpanSingleton_eq_bot_iff {R : Type u_1} [Semiring R] {x : R} : (toSpanSingleton R R x).ker = ⊥ ↔ x ∈ nonZeroDivisorsRight R

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₂] {σ₁₂ : R →+* R₂} {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂} : 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₂] {σ₁₂ : R →+* R₂} {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂} (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₂] {σ₁₂ : R →+* R₂} {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂} (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₂] {σ₁₂ : R →+* R₂} {s : Set M} {f g : M →ₛₗ[σ₁₂] M₂} (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₂] {σ₁₂ : R →+* R₂} {ι : Sort u_8} {v : ι → M} {f g : M →ₛₗ[σ₁₂] M₂} (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} [Semiring R] [AddCommMonoid M] [Module R M] [IsDomain R] [Module.IsTorsionFree R M] {x : M} (h : x ≠ 0) : (toSpanSingleton R M x).ker = ⊥

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) : K ∙ x ⊔ f.ker = ⊤

noncomputable def LinearEquiv.toSpanNonzeroSingleton (R : Type u_1) (M : Type u_4) [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) : R ≃ₗ[R] ↥(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$.

@[simp]

theorem LinearEquiv.toSpanNonzeroSingleton_apply (R : Type u_1) (M : Type u_4) [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree 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] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) (m : ↥(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] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree 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] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) : ↥(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$.

theorem LinearEquiv.coord_self (R : Type u_1) (M : Type u_4) [Ring R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree 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] [IsDomain R] [AddCommGroup M] [Module R M] [Module.IsTorsionFree R M] (x : M) (h : x ≠ 0) (y : ↥(R ∙ x)) : (coord R M x h) y • x = ↑y