LeanPool.VirasoroProject.ToMathlib.LinearAlgebra.Basis.FinsumRepr

theorem smul_support_subset_left {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [AddCommGroup M] [Module R M] (v : ι → M) (cf : ι → R) : (Function.support fun (i : ι) => cf i • v i) ⊆ Function.support cf

theorem finsum_mem_span {ι : Type u_1} {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] (vs : ι → V) (cfs : ι → R) : ∑ᶠ (i : ι), cfs i • vs i ∈ Submodule.span R (Set.range vs)

theorem finsum_mem_mem_span {ι : Type u_1} {R : Type u_2} {V : Type u_3} [Semiring R] [AddCommMonoid V] [Module R V] (vs : ι → V) (cfs : ι → R) (s : Set ι) : ∑ᶠ (i : ι) (_ : i ∈ s), cfs i • vs i ∈ Submodule.span R (vs '' s)

theorem Module.Basis.iSupIndep_submodule_span_of_pairwise_disjoint {R : Type u_1} {M : Type u_2} {ι : Type u_3} {κ : Type u_4} [Semiring R] [AddCommGroup M] [Module R M] (B : Basis ι R M) (Is : κ → Set ι) (Is_disj : Pairwise fun (k₁ k₂ : κ) => Disjoint (Is k₁) (Is k₂)) : iSupIndep fun (k : κ) => Submodule.span R (⇑B '' Is k)

theorem Module.Basis.finsum_repr_smul_basis {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [Nontrivial R] [IsCancelMulZero R] [AddCommGroup M] [Module R M] [IsTorsionFree R M] (B : Basis ι R M) (v : M) : ∑ᶠ (i : ι), (B.repr v) i • B i = v

theorem Module.Basis.repr_finsum {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [Nontrivial R] [IsCancelMulZero R] [AddCommGroup M] [Module R M] [IsTorsionFree R M] (B : Basis ι R M) (cf : ι →₀ R) : B.repr (∑ᶠ (i : ι), cf i • B i) = cf

theorem Module.Basis.repr_finsum_mem_eq_ite {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [Nontrivial R] [IsCancelMulZero R] [AddCommGroup M] [Module R M] [IsTorsionFree R M] (B : Basis ι R M) (cf : ι →₀ R) (I : Set ι) [DecidablePred fun (i : ι) => i ∈ I] (j : ι) : (B.repr (∑ᶠ (i : ι) (_ : i ∈ I), cf i • B i)) j = if j ∈ I then cf j else 0

noncomputable def Module.Basis.basisSubmoduleSpan {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [Nontrivial R] [IsCancelMulZero R] [AddCommGroup M] [Module R M] [IsTorsionFree R M] (B : Basis ι R M) (I : Set ι) : Basis (↑I) R ↥(Submodule.span R (⇑B '' I))

The basis on the span of a subset of a basis, indexed by that subset.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Module.Basis.basis_submodule_span_apply {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Semiring R] [Nontrivial R] [IsCancelMulZero R] [AddCommGroup M] [Module R M] [IsTorsionFree R M] (B : Basis ι R M) (I : Set ι) (i : ↑I) : ↑((B.basisSubmoduleSpan I) i) = B ↑i