# mathlibdocumentation

linear_algebra.span

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

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

## Notations #

• We introduce the notation R ∙ v for the span of a singleton, submodule.span R {v}. This is \., not the same as the scalar multiplication •/\bub.
def submodule.span (R : Type u_1) {M : Type u_4} [semiring R] [ M] (s : set M) :
M

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

Equations
Instances for ↥submodule.span
theorem submodule.mem_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} {s : set M} :
x ∀ (p : M), s px p
theorem submodule.subset_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
s s)
theorem submodule.span_le {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} {p : M} :
p s p
theorem submodule.span_mono {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s t : set M} (h : s t) :
theorem submodule.span_eq_of_le {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p : M) {s : set M} (h₁ : s p) (h₂ : p ) :
= p
theorem submodule.span_eq {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p : M) :
= p
theorem submodule.span_eq_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s t : set M} (hs : s t)) (ht : t s)) :
=
@[simp]
theorem submodule.span_coe_eq_restrict_scalars {R : Type u_1} {M : Type u_4} {S : Type u_7} [semiring R] [ M] (p : M) [semiring S] [ R] [ M] [ M] :

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

theorem submodule.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) :
s) = (f '' s)
theorem linear_map.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) :
s) = (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] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) (N : M₂) :
s) N ∀ (m : M), m sf m N
theorem linear_map.map_span_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) (N : M₂) :
s) N ∀ (m : M), m sf m N

Alias of submodule.map_span_le.

@[simp]
theorem submodule.span_insert_zero {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
s) =
theorem submodule.span_preimage_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M₂) :
(f ⁻¹' s) s)
theorem linear_map.span_preimage_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M₂) :
(f ⁻¹' s) s)

Alias of submodule.span_preimage_le.

theorem submodule.closure_subset_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
s)
theorem submodule.closure_le_to_add_submonoid_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
@[simp]
theorem submodule.span_closure {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
theorem submodule.span_induction {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} {s : set M} {p : M → Prop} (h : x ) (Hs : ∀ (x : M), x sp x) (H0 : p 0) (H1 : ∀ (x y : M), p xp yp (x + y)) (H2 : ∀ (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] [ M] {s : set M} {p : Π (x : M), x → Prop} (Hs : ∀ (x : M) (h : x s), p x _) (H0 : p 0 _) (H1 : ∀ (x : M) (hx : x s) (y : M) (hy : y s), p x hxp y hyp (x + y) _) (H2 : ∀ (a : R) (x : M) (hx : x s), p x hxp (a x) _) {x : M} (hx : x ) :
p x hx

A dependent version of submodule.span_induction.

@[simp]
theorem submodule.span_span_coe_preimage {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
theorem submodule.span_nat_eq_add_submonoid_closure {M : Type u_4} (s : set M) :
@[simp]
theorem submodule.span_nat_eq {M : Type u_4} (s : add_submonoid M) :
theorem submodule.span_int_eq_add_subgroup_closure {M : Type u_1} (s : set M) :
@[simp]
theorem submodule.span_int_eq {M : Type u_1} (s : add_subgroup M) :
@[protected]
def submodule.gi (R : Type u_1) (M : Type u_4) [semiring R] [ M] :

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

Equations
@[simp]
theorem submodule.span_empty {R : Type u_1} {M : Type u_4} [semiring R] [ M] :
@[simp]
theorem submodule.span_univ {R : Type u_1} {M : Type u_4} [semiring R] [ M] :
theorem submodule.span_union {R : Type u_1} {M : Type u_4} [semiring R] [ M] (s t : set M) :
(s t) =
theorem submodule.span_Union {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (s : ι → set M) :
(⋃ (i : ι), s i) = ⨆ (i : ι), (s i)
theorem submodule.span_Union₂ {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} {κ : ι → Sort u_3} (s : Π (i : ι), κ iset M) :
(⋃ (i : ι) (j : κ i), s i j) = ⨆ (i : ι) (j : κ i), (s i j)
theorem submodule.span_attach_bUnion {R : Type u_1} {M : Type u_4} [semiring R] [ M] [decidable_eq M] {α : Type u_2} (s : finset α) (f : s → ) :
(s.attach.bUnion f) = ⨆ (x : s), (f x)
theorem submodule.sup_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p : M) {s : set M} :
p = (p s)
theorem submodule.span_sup {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p : M) {s : set M} :
p = (s p)
theorem submodule.span_eq_supr_of_singleton_spans {R : Type u_1} {M : Type u_4} [semiring R] [ M] (s : set M) :
= ⨆ (x : M) (H : x s), {x}
theorem submodule.span_range_eq_supr {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Type u_2} {v : ι → M} :
(set.range v) = ⨆ (i : ι), {v i}
theorem submodule.span_smul_le {R : Type u_1} {M : Type u_4} [semiring R] [ M] (s : set M) (r : R) :
(r s)
theorem submodule.subset_span_trans {R : Type u_1} {M : Type u_4} [semiring R] [ M] {U V W : set M} (hUV : U V)) (hVW : V W)) :
U W)
theorem submodule.span_smul_eq_of_is_unit {R : Type u_1} {M : Type u_4} [semiring R] [ M] (s : set M) (r : R) (hr : is_unit r) :
(r s) =

See submodule.span_smul_eq (in ring_theory.ideal.operations) for span R (r • s) = r • span R s that holds for arbitrary r in a comm_semiring.

@[simp]
theorem submodule.coe_supr_of_directed {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} [hι : nonempty ι] (S : ι → M) (H : S) :
(supr S) = ⋃ (i : ι), (S i)
@[simp]
theorem submodule.mem_supr_of_directed {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} [nonempty ι] (S : ι → M) (H : S) {x : M} :
x supr S ∃ (i : ι), x S i
theorem submodule.mem_Sup_of_directed {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M)} {z : M} (hs : s.nonempty) (hdir : s) :
z ∃ (y : M) (H : y s), z y
@[simp, norm_cast]
theorem submodule.coe_supr_of_chain {R : Type u_1} {M : Type u_4} [semiring R] [ M] (a : →o M) :
(⨆ (k : ), a k) = ⋃ (k : ), (a k)
theorem submodule.coe_scott_continuous {R : Type u_1} {M : Type u_4} [semiring R] [ M] :

We can regard coe_supr_of_chain as the statement that coe : (submodule R M) → set M is Scott continuous for the ω-complete partial order induced by the complete lattice structures.

@[simp]
theorem submodule.mem_supr_of_chain {R : Type u_1} {M : Type u_4} [semiring R] [ M] (a : →o 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] [ M] {x : M} {p p' : M} :
x p p' ∃ (y : M) (H : y p) (z : M) (H : z p'), y + z = x
theorem submodule.mem_sup' {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} {p p' : M} :
x p p' ∃ (y : p) (z : p'), y + z = x
theorem submodule.coe_sup {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p p' : M) :
(p p') = p + p'
theorem submodule.sup_to_add_submonoid {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p p' : M) :
theorem submodule.sup_to_add_subgroup {R : Type u_1} {M : Type u_2} [ring R] [ M] (p p' : M) :
theorem submodule.mem_span_singleton_self {R : Type u_1} {M : Type u_4} [semiring R] [ M] (x : M) :
x {x}
theorem submodule.nontrivial_span_singleton {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} (h : x 0) :
theorem submodule.mem_span_singleton {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x y : M} :
x {y} ∃ (a : R), a y = x
theorem submodule.le_span_singleton_iff {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : M} {v₀ : M} :
s {v₀} ∀ (v : M), v s(∃ (r : R), r v₀ = v)
theorem submodule.span_singleton_eq_top_iff (R : Type u_1) {M : Type u_4} [semiring R] [ M] (x : M) :
{x} = ∀ (v : M), ∃ (r : R), r x = v
@[simp]
theorem submodule.span_zero_singleton (R : Type u_1) {M : Type u_4} [semiring R] [ M] :
{0} =
theorem submodule.span_singleton_eq_range (R : Type u_1) {M : Type u_4} [semiring R] [ M] (y : M) :
{y}) = set.range (λ (_x : R), _x y)
theorem submodule.span_singleton_smul_le (R : Type u_1) {M : Type u_4} [semiring R] [ M] {S : Type u_2} [monoid S] [ R] [ M] [ M] (r : S) (x : M) :
{r x} {x}
theorem submodule.span_singleton_group_smul_eq (R : Type u_1) {M : Type u_4} [semiring R] [ M] {G : Type u_2} [group G] [ R] [ M] [ M] (g : G) (x : M) :
{g x} = {x}
theorem submodule.span_singleton_smul_eq {R : Type u_1} {M : Type u_4} [semiring R] [ M] {r : R} (hr : is_unit r) (x : M) :
{r x} = {x}
theorem submodule.disjoint_span_singleton {K : Type u_1} {E : Type u_2} [ E] {s : E} {x : E} :
{x}) x sx = 0
theorem submodule.disjoint_span_singleton' {K : Type u_1} {E : Type u_2} [ E] {p : E} {x : E} (x0 : x 0) :
{x}) x p
theorem submodule.mem_span_singleton_trans {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x y z : M} (hxy : x {y}) (hyz : y {z}) :
x {z}
theorem submodule.mem_span_insert {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} {s : set M} {y : M} :
x s) ∃ (a : R) (z : M) (H : z s), x = a y + z
theorem submodule.span_insert {R : Type u_1} {M : Type u_4} [semiring R] [ M] (x : M) (s : set M) :
s) = {x}
theorem submodule.span_insert_eq_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} {s : set M} (h : x ) :
s) =
theorem submodule.span_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
s) =
theorem submodule.span_le_restrict_scalars (R : Type u_1) {M : Type u_4} (S : Type u_7) [semiring R] [ M] (s : set M) [semiring S] [ S] [ M] [ 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] [ M] (s : set M) [semiring S] [ S] [ M] [ M] :
s) s)

A version of submodule.span_le_restrict_scalars with coercions.

theorem submodule.span_span_of_tower (R : Type u_1) {M : Type u_4} (S : Type u_7) [semiring R] [ M] (s : set M) [semiring S] [ S] [ M] [ M] :
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_bot {R : Type u_1} {M : Type u_4} [semiring R] [ M] {s : set M} :
= ∀ (x : M), x sx = 0
@[simp]
theorem submodule.span_singleton_eq_bot {R : Type u_1} {M : Type u_4} [semiring R] [ M] {x : M} :
{x} = x = 0
@[simp]
theorem submodule.span_zero {R : Type u_1} {M : Type u_4} [semiring R] [ M] :
theorem submodule.span_singleton_eq_span_singleton {R : Type u_1} {M : Type u_2} [ring R] [ M] {x y : M} :
{x} = {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] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] {s : set M} [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) :
(f '' s) = 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] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : set M} (h : x ) :
f x (f '' s)
@[simp]
theorem submodule.map_subtype_span_singleton {R : Type u_1} {M : Type u_4} [semiring R] [ M] {p : M} (x : p) :
{x}) = {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] [ M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : set M} (h : f x (f '' s)) :
x

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

theorem submodule.supr_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (p : ι → set M) :
(⨆ (i : ι), (p i)) = (⋃ (i : ι), p i)
theorem submodule.supr_eq_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (p : ι → M) :
(⨆ (i : ι), p i) = (⋃ (i : ι), (p i))
theorem submodule.supr_to_add_submonoid {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (p : ι → M) :
(⨆ (i : ι), p i).to_add_submonoid = ⨆ (i : ι), (p i).to_add_submonoid
theorem submodule.supr_induction {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (p : ι → M) {C : M → Prop} {x : M} (hx : x ⨆ (i : ι), p i) (hp : ∀ (i : ι) (x : M), x p iC 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.supr_induction' {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (p : ι → M) {C : Π (x : M), (x ⨆ (i : ι), p i) → Prop} (hp : ∀ (i : ι) (x : M) (H : x p i), C x _) (h0 : C 0 _) (hadd : ∀ (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.supr_induction.

@[simp]
theorem submodule.span_singleton_le_iff_mem {R : Type u_1} {M : Type u_4} [semiring R] [ M] (m : M) (p : M) :
{m} p m p
theorem submodule.singleton_span_is_compact_element {R : Type u_1} {M : Type u_4} [semiring R] [ M] (x : M) :
theorem submodule.finset_span_is_compact_element {R : Type u_1} {M : Type u_4} [semiring R] [ M] (S : finset M) :

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

theorem submodule.finite_span_is_compact_element {R : Type u_1} {M : Type u_4} [semiring R] [ M] (S : set M) (h : S.finite) :

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

@[protected, instance]
def submodule.is_compactly_generated {R : Type u_1} {M : Type u_4} [semiring R] [ M] :
theorem submodule.submodule_eq_Sup_le_nonzero_spans {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p : M) :
p = has_Sup.Sup {T : M | ∃ (m : M) (hm : m p) (hz : m 0), T = {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] [ M] {I : M} {a : M} :
I < I {a} a I
theorem submodule.mem_supr {R : Type u_1} {M : Type u_4} [semiring R] [ M] {ι : Sort u_2} (p : ι → M) {m : M} :
(m ⨆ (i : ι), p i) ∀ (N : M), (∀ (i : ι), p i N)m N
theorem submodule.mem_span_finite_of_mem_span {R : Type u_1} {M : Type u_4} [semiring R] [ M] {S : set M} {x : M} (hx : x ) :
∃ (T : finset M), T S x

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] [ M] (p : M) {M' : Type u_8} [add_comm_monoid M'] [ M'] (q₁ : M') :
(M × M')

The product of two submodules is a submodule.

Equations
@[simp]
theorem submodule.prod_coe {R : Type u_1} {M : Type u_4} [semiring R] [ M] (p : M) {M' : Type u_8} [add_comm_monoid M'] [ M'] (q₁ : M') :
(p.prod q₁) = p ×ˢ q₁
@[simp]
theorem submodule.mem_prod {R : Type u_1} {M : Type u_4} [semiring R] [ M] {M' : Type u_8} [add_comm_monoid M'] [ M'] {p : M} {q : M'} {x : M × M'} :
x p.prod q x.fst p x.snd q
theorem submodule.span_prod_le {R : Type u_1} {M : Type u_4} [semiring R] [ M] {M' : Type u_8} [add_comm_monoid M'] [ M'] (s : set M) (t : set M') :
(s ×ˢ t) s).prod t)
@[simp]
theorem submodule.prod_top {R : Type u_1} {M : Type u_4} [semiring R] [ M] {M' : Type u_8} [add_comm_monoid M'] [ M'] :
@[simp]
theorem submodule.prod_bot {R : Type u_1} {M : Type u_4} [semiring R] [ M] {M' : Type u_8} [add_comm_monoid M'] [ M'] :
theorem submodule.prod_mono {R : Type u_1} {M : Type u_4} [semiring R] [ M] {M' : Type u_8} [add_comm_monoid M'] [ M'] {p p' : M} {q q' : 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] [ M] (p p' : M) {M' : Type u_8} [add_comm_monoid M'] [ M'] (q₁ q₁' : 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] [ M] (p p' : M) {M' : Type u_8} [add_comm_monoid M'] [ M'] (q₁ q₁' : 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] [ M] (s : set M) :
(-s) =
theorem submodule.mem_span_insert' {R : Type u_1} {M : Type u_4} [ring R] [ M] {x y : M} {s : set M} :
x s) ∃ (a : R), x + a y
@[protected, instance]
def submodule.is_modular_lattice {R : Type u_1} {M : Type u_4} [ring R] [ M] :
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₂] [ M] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : τ₁₂ M M₂] (f : F) (p : M) :
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₂] [ M] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : τ₁₂ M M₂] {f : F} {p : M} (h : p) :
p) = p
@[protected]
theorem linear_map.map_le_map_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : τ₁₂ M M₂] (f : F) {p p' : M} :
p' p p'
theorem linear_map.map_le_map_iff' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : τ₁₂ M M₂] {f : F} (hf : = ) {p p' : M} :
p' p p'
theorem linear_map.map_injective {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : τ₁₂ M M₂] {f : F} (hf : = ) :
theorem linear_map.map_eq_top_iff {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [semiring R₂] [add_comm_group M₂] [ M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : τ₁₂ M M₂] {f : F} (hf : = ) {p : M} :
@[simp]
theorem linear_map.to_span_singleton_apply (R : Type u_1) (M : Type u_4) [semiring R] [ M] (x : M) (b : R) :
x) b = b x
def linear_map.to_span_singleton (R : Type u_1) (M : Type u_4) [semiring R] [ M] (x : M) :

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

Equations
theorem linear_map.span_singleton_eq_range (R : Type u_1) (M : Type u_4) [semiring R] [ M] (x : M) :
{x} =

The range of to_span_singleton x is the span of x.

@[simp]
theorem linear_map.to_span_singleton_one (R : Type u_1) (M : Type u_4) [semiring R] [ M] (x : M) :
x) 1 = x
@[simp]
theorem linear_map.to_span_singleton_zero (R : Type u_1) (M : Type u_4) [semiring R] [ M] :
theorem linear_map.eq_on_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (H : g s) ⦃x : M⦄ (h : x ) :
f x = g x

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

See also linear_map.eq_on_span' for a version using set.eq_on.

theorem linear_map.eq_on_span' {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (H : g s) :
g s)

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

This version uses set.eq_on, and the hidden argument will expand to h : x ∈ (span R s : set M). See linear_map.eq_on_span for a version that takes h : x ∈ span R s as an argument.

theorem linear_map.ext_on {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (hv : = ) (h : g s) :
f = g

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

theorem linear_map.ext_on_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [ M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_3} {v : ι → M} {f g : M →ₛₗ[σ₁₂] M₂} (hv : (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 linear_map.span_singleton_sup_ker_eq_top {K : Type u_3} {V : Type u_6} [field K] [ V] (f : V →ₗ[K] K) {x : V} (hx : f x 0) :
{x} =
theorem linear_map.ker_to_span_singleton (K : Type u_3) (V : Type u_6) [field K] [ V] {x : V} (h : x 0) :
noncomputable def linear_equiv.to_span_nonzero_singleton (K : Type u_3) (V : Type u_6) [field K] [ V] (x : V) (h : x 0) :
K ≃ₗ[K] {x})

Given a nonzero element x of a vector space V over a field K, the natural map from K to the span of x, with invertibility check to consider it as an isomorphism.

Equations
• = {x}) _)
theorem linear_equiv.to_span_nonzero_singleton_one (K : Type u_3) (V : Type u_6) [field K] [ V] (x : V) (h : x 0) :
1 = x, _⟩
@[reducible]
noncomputable def linear_equiv.coord (K : Type u_3) (V : Type u_6) [field K] [ V] (x : V) (h : x 0) :
{x}) ≃ₗ[K] K

Given a nonzero element x of a vector space V over a field K, the natural map from the span of x to K.

theorem linear_equiv.coord_self (K : Type u_3) (V : Type u_6) [field K] [ V] (x : V) (h : x 0) :
x h) x, _⟩ = 1