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.
Vector space over a field
Definition
Let be a field (Field), with additive identity , multiplicative identity , and the field axioms as stated there. A vector space over , also called an -vector space, consists of
- a set , whose elements are called vectors;
- a binary operation on (Binary operation on a set; associativity, commutativity, and a subset closed under the operation), the vector addition;
- an element , the zero vector;
- a map , the scalar multiplication, written ;
subject to the following axioms, in which and are arbitrary.
- (V1) is an abelian group (Group and abelian group): is associative and commutative, is a two-sided identity for (Left identity, right identity, and two-sided identity for a binary operation), and every has an additive inverse (Left inverse, right inverse, and invertible element of a monoid).
- (V2) .
- (V3) .
- (V4) .
- (V5) .
The elements of are called scalars. When several vector spaces are in play we write for the zero of , and we write for the additive inverse of and .
The notation and is legitimate. Axiom (V1) asserts only that some two-sided identity and some additive inverses exist. That there is at most one two-sided identity for is A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity, and that an invertible element of a monoid has exactly one inverse is In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided; both are proved before Group and abelian group and are inherited here with the group structure. So and denote well-defined elements, and nothing below re-derives them.
What (V1) buys, and why it is not restated. Associativity, commutativity, the identity law , the inverse law , cancellation (Cancellation in a group: or forces ; equivalently left and right translation by are bijections of , so and each have exactly one solution) and the inverse identities (In a group , and , the order of the last product being essential) are facts about abelian groups. They are quoted from the group page wherever they are used and are never proved again for vectors.
Remarks
-
Scalar multiplication is not a binary operation on a set. It is a map with arguments from two different sets, so Binary operation on a set; associativity, commutativity, and a subset closed under the operation, which is about a map , does not apply to it and is never cited for it. The definition above cites that item for the vector addition only. In particular "closed under scalar multiplication" below always means for and , which is not an instance of the closure condition defined there.
-
(V5) is an axiom, not a consequence of (V2)–(V4). Take any abelian group and define for every and . Then (V2), (V3) and (V4) all hold, both sides of each being , while (V5) fails as soon as . So (V5) has to be imposed, and it is what ties the scalar action to the identity of .
-
Two structures, one set. A vector space is data: the set , the addition, the zero, and the scalar multiplication, over a fixed field . The same set may carry vector-space structures over different fields, and the field is part of the statement of every result below. A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars is the first place where that matters.
-
The field is the published one. No field axiom is restated here; is a field in the sense of Field, whose axiom (A) already says that is an abelian group and whose axiom (M) says the same of . In particular every field is a vector space over itself, which is A field is a vector space over itself, and over any subfield every -vector space is a -vector space by restricting the scalars.
Depends on
Field
Group and abelian group
Binary operation on a set; associativity, commutativity, and a subset closed under the operation
Left identity, right identity, and two-sided identity for a binary operation
Left inverse, right inverse, and invertible element of a monoid
A left identity and a right identity for the same binary operation are equal; hence there is at most one two-sided identity
In a monoid, a left inverse and a right inverse of the same element are equal; hence an invertible element has exactly one inverse, and it is two-sided