Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicableSession-authored (Fable 5 assisted)judge pass (z-ai/glm-5.2)audited 2026-07-28
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis

Definition

Let VV be a vector space over a field FF (Vector space over a field).

A subset BVB \subseteq V is a basis of VV when

The empty set is a basis of the zero space, and of nothing else. \varnothing is linearly independent (Linear independence: a finite list v:nVv : n \to V is independent when i<nλivi=0V\sum_{i<n} \lambda_i v_i = 0_V forces every λi=0F\lambda_i = 0_F, and a subset SVS \subseteq V is independent when every injective finite list into SS is independent) and span()={0V}\operatorname{span}(\varnothing) = \{0_V\} (span(S)\operatorname{span}(S) is exactly the set of linear combinations of finite lists of elements of SS, and span()={0V}\operatorname{span}(\varnothing) = \{0_V\}), so \varnothing is a basis of VV exactly when V={0V}V = \{0_V\}. This is the case n=0n = 0 from which every induction on this page starts, and it is a genuine case rather than a convention.

Ordered bases

An ordered basis of VV is a finite list v:nVv : n \to V, with nNn \in \mathbb{N} and n={0,,n1}n = \{0, \dots, n-1\} the von Neumann natural (The natural numbers N\mathbb{N} (von Neumann), On N\mathbb{N} the order is membership: m<n    mnm < n \iff m \in n), such that vv is injective (Injection, surjection, bijection) and its image v[n]v[n] is a basis of VV.

By claim 6 of Finite sums re-indexed along an injection, with a zero term deleted, and concatenated; and the closure properties of linear independence: an independent list is injective and never 0V0_V, its sublists are independent, a list is independent exactly when it is injective with linearly independent image, and every subset of a linearly independent set is linearly independent, a list is linearly independent exactly when it is injective with linearly independent image, so an ordered basis is equally described as a linearly independent list v:nVv : n \to V with span(v[n])=V\operatorname{span}(v[n]) = V: the injectivity does not have to be imposed separately. The empty list is the ordered basis of the zero space.

An ordered basis is a list, so it carries an order; a basis is a set, so it does not. Reordering an ordered basis gives a different ordered basis with the same image, and the coordinates of A finite list v:nVv : n \to V is an ordered basis if and only if every xVx \in V equals i<nλivi\sum_{i<n} \lambda_i v_i for exactly one λ:nF\lambda : n \to F; those scalars are the coordinates of xx in that ordered basis are attached to the list, not to the set.

Bases of a linear subspace

Let UU be a linear subspace of VV (Linear subspace of a vector space), which is itself a vector space over FF, with the addition, the zero vector and the scalar multiplication of VV restricted to UU. For AUA \subseteq U the two readings of "AA is a basis" — computed inside UU, or computed inside VV — agree, so the phrase needs no disambiguation below.

Consequently AUA \subseteq U is a basis of the vector space UU if and only if AA is linearly independent as a subset of VV and span(A)=U\operatorname{span}(A) = U.

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 64 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources