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.
Linear subspace of a vector space
Definition
Let be a vector space over a field (Vector space over a field). A subset is a linear subspace of when
- (W1) ;
- (W2) is closed under the vector addition: implies ;
- (W3) is closed under scalar multiplication: and imply .
Every vector space has the two trivial linear subspaces and itself; a linear subspace with is called proper.
The restricted operations are the required data, and is a vector space. By (W2) the vector addition of restricts to a binary operation , and by (W3) the scalar multiplication restricts to a map . With these and the element , the set is a vector space over :
- axioms (V2)–(V5) are equations required of elements of , which are in particular elements of , so they are inherited from ; likewise associativity and commutativity of the restricted addition;
- lies in by (W1) and is a two-sided identity for the restricted addition, since it is one in ;
- for the vector lies in by (W3), and (In any vector space , , , , and forces or ), so and holds in .
So is an abelian group, which is axiom (V1), and is a vector space over whose zero vector and whose additive inverses are those of . In the language of Subgroup, the three displayed conditions (S1) , (S2) closure under addition and (S3) closure under additive inverses all hold, so is a subgroup of the abelian group (Group and abelian group); that reading, and its converse, are recorded as The additive group of a vector space is an abelian group and every linear subspace is a subgroup of it; conversely a subgroup closed under scalar multiplication is a linear subspace and are cited from there rather than re-argued below.
Remarks
-
"Linear subspace", never bare "subspace", in this library. The word subspace is already in use here for the topological notion, a subset of a topological space carrying the induced topology, which is an unrelated idea. The names on this page therefore all say linear:
def-linear-subspace,lem-linear-subspace-criterion,lem-intersection-of-linear-subspaces,lem-linear-subspace-is-a-subgroup,def-sum-of-linear-subspaces. Where the ambient vector space is fixed and no confusion is possible, the surrounding prose still writes the full phrase. -
Closure under negatives is not a fourth condition. It follows from (W3), because the additive inverse of a vector is the scalar multiple . This is why the definition asks for three conditions where the definition of a subgroup asks for three of its own, and why the one-step test (One-step subspace test: a nonempty is a linear subspace if and only if for all and ) can compress them into one.
-
(W1) cannot be replaced by "" while dropping the others. It can be replaced by nonemptiness given (W3), since a nonempty closed under scalar multiplication contains (In any vector space , , , , and forces or ) for any of its elements . Stated with (W1) the definition is checkable one condition at a time, and the economical single test is One-step subspace test: a nonempty is a linear subspace if and only if for all and .
-
The field matters. A subset of may be closed under the scalars of a subfield without being closed under all of , so "linear subspace" always means "linear subspace over the field named". Restriction of scalars (A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars) is what makes that distinction possible.