Finite spans and one-dimensional lines #
A generator with a unit coefficient in a linear combination can be replaced by that combination without changing the span. Over a division ring, a nonzero vector in the line spanned by another vector can be used to recover that generator's membership in any submodule.
theorem
TauCeti.Submodule.span_insert_erase_eq_span_of_isUnit
{A : Type u_1}
[Ring A]
{M : Type u_2}
[AddCommGroup M]
[Module A M]
[DecidableEq M]
{s : Finset M}
{i x : M}
{f : M → A}
(hi : i ∈ s)
(hf : ∑ a ∈ s, f a • a = x)
(hfi : IsUnit (f i))
:
If one coefficient of x in a finite span is a unit, then x can replace that generator.
theorem
Submodule.mem_of_mem_span_singleton_of_ne_zero
{K : Type u_1}
{V : Type u_2}
[DivisionRing K]
[AddCommGroup V]
[Module K V]
(P : Submodule K V)
{x y : V}
(hx : x ∈ P)
(hx0 : x ≠ 0)
(hxy : x ∈ K ∙ y)
:
If a nonzero member of a submodule lies in the line spanned by y, then y also belongs to
the submodule.