mathlib3 documentation

linear_algebra.span

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Notations #

def submodule.span (R : Type u_1) {M : Type u_4} [semiring R] [add_comm_monoid 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 submodule.span
theorem submodule.mem_span {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} :
x submodule.span R s (p : submodule R M), s p x p
theorem submodule.subset_span {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {s : set M} :
theorem submodule.span_le {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {s : set M} {p : submodule R M} :
theorem submodule.span_mono {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {s t : set M} (h : s t) :
theorem submodule.span_monotone {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :
theorem submodule.span_eq_of_le {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid 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] [add_comm_monoid M] [module R M] (p : submodule R M) :
theorem submodule.span_eq_span {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {s t : set M} (hs : s (submodule.span R t)) (ht : t (submodule.span R s)) :
@[simp]
theorem submodule.span_coe_eq_restrict_scalars {R : Type u_1} {M : Type u_4} {S : Type u_7} [semiring R] [add_comm_monoid M] [module R M] (p : submodule R M) [semiring S] [has_smul S R] [module S M] [is_scalar_tower S R 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] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) :
theorem linear_map.map_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (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] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) (N : submodule R₂ M₂) :
submodule.map f (submodule.span R s) N (m : M), m s f 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] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] [ring_hom_surjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M) (N : submodule R₂ M₂) :
submodule.map f (submodule.span R s) N (m : M), m s 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] [add_comm_monoid 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] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M₂) :
theorem linear_map.span_preimage_le {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] (f : M →ₛₗ[σ₁₂] M₂) (s : set M₂) :

Alias of submodule.span_preimage_le.

@[simp]
theorem submodule.span_induction {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} {p : M Prop} (h : x submodule.span R s) (Hs : (x : M), x s p x) (H0 : p 0) (H1 : (x y : M), p x p y p (x + y)) (H2 : (a : R) (x : M), p x p (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] [add_comm_monoid M] [module R M] {s : set M} {p : Π (x : M), x submodule.span R s Prop} (Hs : (x : M) (h : x s), p x _) (H0 : p 0 _) (H1 : (x : M) (hx : x submodule.span R s) (y : M) (hy : y submodule.span R s), p x hx p y hy p (x + y) _) (H2 : (a : R) (x : M) (hx : x submodule.span R s), p x hx p (a x) _) {x : M} (hx : x submodule.span R s) :
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] [add_comm_monoid M] [module R M] {s : set M} :
@[protected]
def submodule.gi (R : Type u_1) (M : Type u_4) [semiring R] [add_comm_monoid M] [module 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] [add_comm_monoid M] [module R M] :
@[simp]
theorem submodule.span_univ {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :
theorem submodule.span_union {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (s t : set M) :
theorem submodule.span_Union {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (s : ι set M) :
submodule.span R ( (i : ι), s i) = (i : ι), submodule.span R (s i)
theorem submodule.span_Union₂ {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} {κ : ι Sort u_3} (s : Π (i : ι), κ i set M) :
submodule.span R ( (i : ι) (j : κ i), s i j) = (i : ι) (j : κ i), submodule.span R (s i j)
theorem submodule.span_attach_bUnion {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] [decidable_eq M] {α : Type u_2} (s : finset α) (f : s finset M) :
theorem submodule.sup_span {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid 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] [add_comm_monoid M] [module R M] (p : submodule R M) {s : set M} :
theorem submodule.span_eq_supr_of_singleton_spans {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (s : set M) :
submodule.span R s = (x : M) (H : x s), submodule.span R {x}
theorem submodule.span_range_eq_supr {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Type u_2} {v : ι M} :
theorem submodule.span_smul_le {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (s : set M) (r : R) :
theorem submodule.subset_span_trans {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {U V W : set M} (hUV : U (submodule.span R V)) (hVW : V (submodule.span R W)) :
theorem submodule.span_smul_eq_of_is_unit {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (s : set M) (r : R) (hr : is_unit r) :

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] [add_comm_monoid M] [module R M] {ι : Sort u_2} [hι : nonempty ι] (S : ι submodule R M) (H : directed has_le.le S) :
(supr S) = (i : ι), (S i)
@[simp]
theorem submodule.mem_supr_of_directed {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} [nonempty ι] (S : ι submodule R M) (H : directed has_le.le 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] [add_comm_monoid M] [module R M] {s : set (submodule R M)} {z : M} (hs : s.nonempty) (hdir : directed_on has_le.le s) :
z has_Sup.Sup s (y : submodule R 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] [add_comm_monoid M] [module R M] (a : →o submodule R M) :
( (k : ), a k) = (k : ), (a k)

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] [add_comm_monoid 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] [add_comm_monoid M] [module R M] {x : M} {p p' : submodule R 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] [add_comm_monoid M] [module R M] {x : M} {p p' : submodule R 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] [add_comm_monoid M] [module R M] (p p' : submodule R M) :
(p p') = p + p'
theorem submodule.mem_span_singleton_self {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (x : M) :
theorem submodule.nontrivial_span_singleton {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x : M} (h : x 0) :
theorem submodule.mem_span_singleton {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x 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] [add_comm_monoid M] [module R M] {s : submodule R M} {v₀ : M} :
s submodule.span R {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] [add_comm_monoid 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] [add_comm_monoid M] [module R M] :
theorem submodule.span_singleton_eq_range (R : Type u_1) {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] (y : M) :
(submodule.span R {y}) = set.range (λ (_x : R), _x y)
theorem submodule.span_singleton_smul_le (R : Type u_1) {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {S : Type u_2} [monoid S] [has_smul S R] [mul_action S M] [is_scalar_tower S R M] (r : S) (x : M) :
theorem submodule.span_singleton_group_smul_eq (R : Type u_1) {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {G : Type u_2} [group G] [has_smul G R] [mul_action G M] [is_scalar_tower G R M] (g : G) (x : M) :
theorem submodule.span_singleton_smul_eq {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {r : R} (hr : is_unit r) (x : M) :
theorem submodule.disjoint_span_singleton {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {s : submodule K E} {x : E} :
disjoint s (submodule.span K {x}) x s x = 0
theorem submodule.disjoint_span_singleton' {K : Type u_1} {E : Type u_2} [division_ring K] [add_comm_group E] [module K E] {p : submodule K E} {x : E} (x0 : x 0) :
theorem submodule.mem_span_singleton_trans {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x y z : M} (hxy : x submodule.span R {y}) (hyz : y submodule.span R {z}) :
theorem submodule.mem_span_insert {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x : M} {s : set M} {y : M} :
x submodule.span R (has_insert.insert y s) (a : R) (z : M) (H : z submodule.span R s), x = a y + z
theorem submodule.mem_span_pair {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x y z : M} :
z submodule.span R {x, y} (a b : R), a x + b y = z
theorem submodule.span_insert {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid 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] [add_comm_monoid 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] [add_comm_monoid M] [module R M] {s : set M} :
theorem submodule.span_le_restrict_scalars (R : Type u_1) {M : Type u_4} (S : Type u_7) [semiring R] [add_comm_monoid M] [module R M] (s : set M) [semiring S] [has_smul R S] [module S M] [is_scalar_tower 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] [add_comm_monoid M] [module R M] (s : set M) [semiring S] [has_smul R S] [module S M] [is_scalar_tower R S M] :

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] [add_comm_monoid M] [module R M] (s : set M) [semiring S] [has_smul R S] [module S M] [is_scalar_tower 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] [add_comm_monoid M] [module R M] {s : set M} :
submodule.span R s = (x : M), x s x = 0
@[simp]
theorem submodule.span_singleton_eq_bot {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {x : M} :
@[simp]
theorem submodule.span_zero {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] :
theorem submodule.span_singleton_eq_span_singleton {R : Type u_1} {M : Type u_2} [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] {x y : M} :
submodule.span R {x} = submodule.span 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] [add_comm_monoid M] [module R M] [semiring R₂] {σ₁₂ : R →+* R₂} [add_comm_monoid M₂] [module R₂ M₂] {s : set M} [ring_hom_surjective σ₁₂] (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] [add_comm_monoid M] [module 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 submodule.span R s) :
f x submodule.span R₂ (f '' s)
@[simp]
theorem submodule.map_subtype_span_singleton {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {p : submodule R M} (x : p) :
theorem submodule.not_mem_span_of_apply_not_mem_span_image {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [add_comm_monoid M] [module 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 submodule.span R₂ (f '' s)) :

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] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι set M) :
( (i : ι), submodule.span R (p i)) = submodule.span R ( (i : ι), p i)
theorem submodule.supr_eq_span {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι submodule R M) :
( (i : ι), p i) = submodule.span R ( (i : ι), (p i))
theorem submodule.supr_to_add_submonoid {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι submodule R 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] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι submodule R M) {C : M Prop} {x : M} (hx : x (i : ι), p i) (hp : (i : ι) (x : M), x p i C x) (h0 : C 0) (hadd : (x y : M), C x C y C (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] [add_comm_monoid M] [module R M] {ι : Sort u_2} (p : ι submodule R 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 hx C y hy C (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] [add_comm_monoid M] [module R M] (m : M) (p : submodule R M) :

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.

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

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] [add_comm_monoid M] [module R M] (p : submodule R M) {M' : Type u_8} [add_comm_monoid M'] [module R M'] (q₁ : submodule R M') :
submodule R (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] [add_comm_monoid M] [module R M] (p : submodule R M) {M' : Type u_8} [add_comm_monoid 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] [add_comm_monoid M] [module R M] {M' : Type u_8} [add_comm_monoid M'] [module R M'] {p : submodule R M} {q : submodule R 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] [add_comm_monoid M] [module R M] {M' : Type u_8} [add_comm_monoid 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] [add_comm_monoid M] [module R M] {M' : Type u_8} [add_comm_monoid M'] [module R M'] :
@[simp]
theorem submodule.prod_bot {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_8} [add_comm_monoid M'] [module R M'] :
theorem submodule.prod_mono {R : Type u_1} {M : Type u_4} [semiring R] [add_comm_monoid M] [module R M] {M' : Type u_8} [add_comm_monoid 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] [add_comm_monoid M] [module R M] (p p' : submodule R M) {M' : Type u_8} [add_comm_monoid 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] [add_comm_monoid M] [module R M] (p p' : submodule R M) {M' : Type u_8} [add_comm_monoid M'] [module R M'] (q₁ 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] [add_comm_group M] [module R M] (s : set M) :
theorem submodule.mem_span_insert' {R : Type u_1} {M : Type u_4} [ring R] [add_comm_group M] [module R M] {x y : M} {s : set M} :
@[protected, instance]
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₂] [add_comm_group M] [module R M] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : semilinear_map_class 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₂] [add_comm_group M] [module R M] [add_comm_group M₂] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : semilinear_map_class F τ₁₂ M M₂] {f : F} {p : submodule R M} (h : linear_map.ker f 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] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : semilinear_map_class F τ₁₂ M M₂] (f : F) {p p' : submodule R M} :
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] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : semilinear_map_class F τ₁₂ M M₂] {f : F} (hf : linear_map.ker f = ) {p p' : submodule R M} :
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] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : semilinear_map_class F τ₁₂ M M₂] {f : F} (hf : linear_map.ker f = ) :
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] [add_comm_group M₂] [module R M] [module R₂ M₂] {τ₁₂ : R →+* R₂} [ring_hom_surjective τ₁₂] {F : Type u_8} [sc : semilinear_map_class F τ₁₂ M M₂] {f : F} (hf : linear_map.range f = ) {p : submodule R M} :
@[simp]
theorem linear_map.to_span_singleton_apply (R : Type u_1) (M : Type u_4) [semiring R] [add_comm_monoid M] [module R M] (x : M) (b : R) :
def linear_map.to_span_singleton (R : Type u_1) (M : Type u_4) [semiring R] [add_comm_monoid 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.

Equations

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] [add_comm_monoid M] [module R M] (x : M) :
@[simp]
theorem linear_map.eq_on_span {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (H : set.eq_on 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 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] [add_comm_monoid M] [module R M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (H : set.eq_on f 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] [add_comm_monoid M] [module R M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {s : set M} {f g : M →ₛₗ[σ₁₂] M₂} (hv : submodule.span R s = ) (h : set.eq_on 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 linear_map.ext_on_range {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [semiring R] [add_comm_monoid M] [module R M] [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] {σ₁₂ : R →+* R₂} {ι : Type u_3} {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 linear_map.span_singleton_sup_ker_eq_top {K : Type u_3} {V : Type u_6} [field K] [add_comm_group V] [module K V] (f : V →ₗ[K] K) {x : V} (hx : f x 0) :
noncomputable def linear_equiv.to_span_nonzero_singleton (R : Type u_1) (M : Type u_4) [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (x : M) (h : x 0) :

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

Equations
theorem linear_equiv.to_span_nonzero_singleton_one (R : Type u_1) (M : Type u_4) [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (x : M) (h : x 0) :
@[reducible]
noncomputable def linear_equiv.coord (R : Type u_1) (M : Type u_4) [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (x : M) (h : x 0) :

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

theorem linear_equiv.coord_self (R : Type u_1) (M : Type u_4) [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (x : M) (h : x 0) :
(linear_equiv.coord R M x h) x, _⟩ = 1
theorem linear_equiv.coord_apply_smul (R : Type u_1) (M : Type u_4) [ring R] [add_comm_group M] [module R M] [no_zero_smul_divisors R M] (x : M) (h : x 0) (y : (submodule.span R {x})) :