noncomputable def Basis.spanImage {ι : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {s : Set ι} (hli : LinearIndepOn R v s) : Module.Basis (↑s) R ↥(Submodule.span R (v '' s))

Equations

• Basis.spanImage hli = (Module.Basis.span ⋯).map (LinearEquiv.ofEq (Submodule.span R (Set.range fun (x : ↑s) => v ↑x)) (Submodule.span R (v '' s)) ⋯)

@[simp]

theorem Basis.spanImage_apply {ι : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {s : Set ι} (hli : LinearIndepOn R v s) {i : ↑s} : ↑((spanImage hli) i) = v ↑i

noncomputable def Basis.mkImage {ι : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {s : Set ι} (hli : LinearIndepOn R v s) (hsp : ⊤ ≤ Submodule.span R (v '' s)) : Module.Basis (↑s) R M

Equations

• Basis.mkImage hli hsp = Module.Basis.mk ⋯ ⋯

theorem LinearIndepOn.union_of_quotient' {R : Type u_8} {M : Type u_9} {ι : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set ι} {f : ι → M} (hs : LinearIndepOn R f s) (ht : LinearIndepOn R (⇑(Submodule.span R (f '' s)).mkQ ∘ f) t) : LinearIndepOn R f (s ∪ t)

Replace the unprimed version with this.

theorem linearIndepOn_pair_iff' {R : Type u_8} {M : Type u_9} {ι : Type u_10} [Ring R] [AddCommGroup M] [Module R M] {i j : ι} (f : ι → M) (hij : i ≠ j) : LinearIndepOn R f {i, j} ↔ ∀ (c d : R), c • f i = d • f j → c = 0 ∧ d = 0

theorem linearDepOn_pair_iff {K : Type u_8} {V : Type u_9} {ι : Type u_10} [DivisionRing K] [AddCommGroup V] [Module K V] {i j : ι} (f : ι → V) (hij : i ≠ j) : ¬LinearIndepOn K f {i, j} ↔ ∃ (c : K) (d : K), c • f i = d • f j ∧ ¬(c = 0 ∧ d = 0)

@[simp]

theorem Basis.mkImage_apply {ι : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {s : Set ι} (hli : LinearIndepOn R v s) (hsp : ⊤ ≤ Submodule.span R (v '' s)) (i : ↑s) : (mkImage hli hsp) i = v ↑i

@[simp]

theorem Basis.mkImage_repr {ι : Type u_8} {R : Type u_9} {M : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] {v : ι → M} {s : Set ι} (hli : LinearIndepOn R v s) (hsp : ⊤ ≤ Submodule.span R (v '' s)) (x : M) : (mkImage hli hsp).repr x = (LinearIndependent.repr hli) ⟨x, ⋯⟩

@[simp]

theorem Finsupp.ker_lcoeFun {α : Type u_8} {M : Type u_9} {R : Type u_10} [Semiring R] [AddCommMonoid M] [Module R M] : lcoeFun.ker = ⊥

theorem LinearIndepOn.exists_maximal {ι : Type u_8} {R : Type u_9} {M : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s₀ t : Set ι} {v : ι → M} (hli : LinearIndepOn R v s₀) (hs₀t : s₀ ⊆ t) : ∃ (s : Set ι), s₀ ⊆ s ∧ Maximal (fun (r : Set ι) => r ⊆ t ∧ LinearIndepOn R v r) s

noncomputable def LinearIndepOn.extension {ι : Type u_8} {R : Type u_9} {M : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set ι} {v : ι → M} (hli : LinearIndepOn R v s) (hst : s ⊆ t) : Set ι

Equations

• hli.extension hst = ⋯.choose

theorem LinearIndepOn.extension_maximal {ι : Type u_8} {R : Type u_9} {M : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set ι} {v : ι → M} (hli : LinearIndepOn R v s) (hst : s ⊆ t) : Maximal (fun (r : Set ι) => r ⊆ t ∧ LinearIndepOn R v r) (hli.extension hst)

theorem LinearIndepOn.subset_extension {ι : Type u_8} {R : Type u_9} {M : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set ι} {v : ι → M} (hli : LinearIndepOn R v s) (hst : s ⊆ t) : s ⊆ hli.extension hst

theorem LinearIndepOn.span_eq_of_maximal_subset {ι : Type u_8} {R : Type u_9} {M : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s t : Set ι} {v : ι → M} (hmax : Maximal (fun (r : Set ι) => r ⊆ t ∧ LinearIndepOn R v r) s) : Submodule.span R (v '' s) = Submodule.span R (v '' t)

theorem LinearIndepOn.span_eq_top_of_maximal {ι : Type u_8} {R : Type u_9} {M : Type u_10} [DivisionRing R] [AddCommGroup M] [Module R M] {s : Set ι} {v : ι → M} (hmax : Maximal (fun (x : Set ι) => LinearIndepOn R v x) s) : Submodule.span R (v '' s) = Submodule.span R (Set.range v)