Skip to the content

Math 2.0

Vector space

Definition

Let $F$ be a field. A vector space over $F$ is a set $V$ with two maps: an addition $V \times V \to V$ , $(u, v) \mapsto u + v$ , and a scalar multiplication $F \times V \to V$ , $(a, v) \mapsto av$ . These axioms must hold for all $u, v, w \in V$ and $a, b \in F$ :

$u + (v + w) = (u + v) + w$ .
$u + v = v + u$ .
There is an element $0 \in V$ with $v + 0 = v$ for all $v \in V$ .
For each $v \in V$ there is an element $-v \in V$ with $v + (-v) = 0$ .
$a(bv) = (ab)v$ .
$1v = v$ , where $1$ is the unit of $F$ .
$a(u + v) = au + av$ .
$(a + b)v = av + bv$ .

The elements of $V$ are vectors, and the elements of $F$ are scalars.

Remarks

Axioms 1 to 4 say that $(V, +)$ is an abelian group. The axioms give $0v = 0$ and $(-1)v = -v$ for all $v \in V$ . A vector space is a module over a field; Mathlib uses Module F V for both. Examples are the coordinate space $F^n$ , spaces of matrices and function spaces.

Explanations

L1 human

A vector space is a collection of objects that we can add together and stretch by numbers. Arrows in the plane are the standard picture, but polynomials and functions also form vector spaces. The eight axioms list the rules that make the usual algebra work.

What this node needs for W2

edge not_instance_of in: one non-example that fails one clause (0 of 1)

The writing levels say how complete the text of a node is. They do not measure its truth.

What depends on this

226 nodes use this node, directly or through other nodes.

Singular value decomposition 000NPTMX6J
Dimension of the dual space 00889YD15K
Linear map of a matrix 009892PZ30
Scaling a row scales the determinant 009CY8JXFX
Normed vector space 00A0RPAQ8A
Nullity 00K4FK4NBH
Every vector space has a basis 00MS9VMQ9Z
Positive definite quadratic form 00QN1N6MNT
Jordan–Chevalley decomposition 011K11VPJN
Leibniz formula for determinants 016PE4VZ8Q
Finite-dimensional vector space 018W3V3TCT
Inner product space 01EK923SKP
Determinant of a scalar multiple 01EXSMK864
Adding a multiple of one row to another preserves the determinant 01ZTQBK64Q
Reflection 025158VEYZ
Parallelogram law 026HPGYGS4
Rank of a product of matrices 02FDWY55AS
Polar form of a quadratic form 02STTYFBVY
External direct sum 02WZB422CE
Kernel of a linear map 02YFME3RGW
Triangularisation 0363JMQ42Y
Characteristic polynomial 039HF58KQ5
Determinant of a linear map 03F5KP94K0
A matrix is invertible iff its determinant is a unit 03Q7RE2HXR
Direct sum of subspaces 041JTZCK9Q
Rational canonical form 042JWAR3Q0
Parseval's identity 047RFCNVSK
Complementary subspaces 04C3BAHV03
Determinant is multiplicative 04CPJ6AF00
Spectrum of a matrix 04EHB7YDQS
Riesz representation theorem in finite dimensions 04GYPXDXNH
Determinant as signed volume 04X3PR72VJ
Product of a matrix and its adjugate 0528HKWZ1Z
Annihilating polynomial 052M4SX57M
Eigenvalues are the roots of the characteristic polynomial 053QVHF6N7
A matrix is diagonalisable iff it has a basis of eigenvectors 056SW1E0AC
Isomorphism with the coordinate space 059THXBRBB
Polarisation identity 05FKHRT0B4
Dimension 05G2G0P224
Matrix of a composition is the product of matrices 05Q1B7MH0M
Orthogonal family for a bilinear form 05Q4JD6XEH
Composition of linear maps 05YBKMRVAR
Laplace expansion along a column 06AMCJMMVM
Dimension of a direct product 06HN47VPTH
Grassmann's formula 06HTJNCMPA
Spectral theorem 06J4PXRG22
Every spanning set contains a basis 06MRNP4BNT
Dimension of the annihilator 06Q1EFVH0Q
Geometric multiplicity 06YSJVR356
Linear isometry 0717XXPWM6
Symmetric bilinear form 0744CN4MDA
Determinant of the inverse 0783S9D0ZH
Orthogonal complement 079D68S3AW
Generalised eigenspace 07PNDWA7CE
Third isomorphism theorem for vector spaces 07RB3EMBWW
Existence of an eigenvalue over an algebraically closed field 08CJB2NQ92
Exterior algebra 08HK38GCSM
Norm 08NYZ2FS6B
Cauchy–Binet formula 08WE2W7DYS
Steinitz exchange lemma 08ZDRN6H41
Alternating bilinear form 08ZQAKBKHF
An injective endomorphism of a finite-dimensional space is surjective 0912EEEVCT
Minimal polynomial divides the characteristic polynomial 093X6MN6Y6
Linearly independent set of the right size is a basis 096V7H13H9
Cramer's rule 0977KZ6PQB
Coordinates in an orthonormal basis 09DZ8CD1AK
Orthonormal family 09VYHEF2VT
Permuting rows multiplies the determinant by the sign 09YB3WQG38
Determinant of a matrix exponential 0A1QQN333A
Multiplication by a matrix as a linear map 0AJ0KP1B31
Second isomorphism theorem for vector spaces 0APN65D6Y6
Eigenspace 0AYEPBQMAW
Eigenvector 0B5H4208Z9
Rotation matrix 0B9QNFGTHM
Matrix determinant lemma 0BC3Q6K92H
A linear map is injective iff its kernel is trivial 0BJBYCGMWE
Spanning set 0BJKVF90Z6
Coordinate vector 0BMVBHTWV2
Polynomial of an endomorphism 0BNEXSKNRV
Pythagorean theorem in an inner product space 0BVTDM872V
Least squares 0BYTQ4X1HC
Characteristic polynomial of a linear map 0BZ81AJNWF
Laplace expansion along a row 0C08BQ3M05
Determinant is the product of the eigenvalues 0C2F40MEBC
Dual map 0C2TQMW5A1
Determinant 0C3CFHDN6R
Eigenvalues of a self-adjoint operator are real 0C4NT4GT3X
Classification of complex quadratic forms 0CEX9BRXRZ
Special orthogonal group 0CGYNDCWRR
Matrix of the adjoint is the conjugate transpose 0DBTE6HVBD
Spectral theorem for Hermitian matrices 0DGZBQWZWN
Dimension of the orthogonal complement 0E2NYPVSP9
Inverse in terms of the adjugate 0ENVM493VK
Normal operator 0ENZN5G4CV
Invariant subspace 0EP59ESQ94
Row space 0EP73HK4C4
Linear subspace 0EPTJA5QV4
QR decomposition 0ERWG4NXQ9
Gershgorin circle theorem 0ETGP0XVCJ
Linear independence 0EVHJFTG9Z
Rank of a matrix 0EWQEYRVA8
Column space 0F0RPPJ2TT
Cayley–Hamilton theorem 0F765KFC2J
Triangle inequality for norms 0FJZMBX0ZZ
Trace is a coefficient of the characteristic polynomial 0FRYPZ6D0X
Determinant of a matrix with a zero row 0FS6B46E5T
Orthonormal basis 0FWJ0VW561
Sylvester's determinant theorem 0G24VQ1088
Tensor product of vector spaces 0G31VJ5YS5
Adjugate matrix 0GMPYM0NSR
Rule of Sarrus 0H8SZFFDXJ
Eigenvectors with distinct eigenvalues are linearly independent 0HNMFG8F8K
Linear span 0HR573CHNM
Rouché–Capelli theorem 0HV1SKWPMS
Gram matrix 0HX8HZ1WTQ
Eigenvalues of a positive definite matrix are positive 0HYC2RHD3M
Quadratic form 0HZNE5QZDJ
Quotient map 0J0SK5FF4M
Determinant of a block triangular matrix 0J9TVTNB4K
Image of a linear map 0JB228DCWB
Linear combination 0JB3DP1BMF
Rank of a linear map 0JGB7A6GTS
Eigenspaces of a self-adjoint operator are orthogonal 0JHGAV9H25
An orthonormal family is linearly independent 0JWM6GJNQW
Determinant of a triangular matrix 0K1KKMFHYH
Singular value 0K2TX12X58
Determinant of a matrix with two equal rows 0K4VQB7HWR
Rayleigh quotient 0K4WCNTMHG
Determinant via the Schur complement 0KA7A4ENVJ
Nondegenerate bilinear form 0KAN330PAH
Norm induced by an inner product 0KG4D8AP6G
Determinant of a linear map is the determinant of its matrix 0KMN32XGPF
Signature of a quadratic form 0KQZYGEJTF
Change of basis matrix 0KWXYZPJKN
Every linearly independent set extends to a basis 0M4SXE5WW3
Dual space 0M856Q1AMZ
Nilpotent endomorphism 0M8MHYERTY
Self-adjoint operator 0MB8HQW495
Orthogonal projection is the closest point 0MCDDSCB9Z
Product of vector spaces 0MM085RX00
Diagonalisable iff the minimal polynomial has distinct roots 0MPAJRB23T
Change of basis formula 0MQXVZEBMT
Alternating multilinear map 0MSWYWHYF5
First isomorphism theorem for linear maps 0MTBGVZ4XJ
Trace is the sum of the eigenvalues 0NMXDCNNKR
Matrix of a bilinear form 0P24YW565F
Bilinear form 0P799D6AMN
Vandermonde determinant 0P84B554AS
Existence of a complementary subspace 0P9T8WHNMH
Restriction of an endomorphism to an invariant subspace 0PFPWKBDTJ
Determinant is multilinear in the rows 0PPG793642
Null space 0PQ2GGY1QV
Principal axis theorem 0PR5P9Z4KM
Endomorphism 0PTF1PTJK0
Orthogonal complement of the orthogonal complement 0PXN9G4MX1
Orientation of a real vector space 0Q8BZXVT1Z
Orthogonal projection 0Q8HZTJC7G
Cayley–Hamilton theorem for linear maps 0QEM68Y0DE
Eigenvalues are the roots of the minimal polynomial 0QF4ZEFG52
Dimension of the coordinate space 0QK7FPE6VE
Semisimple endomorphism 0QS8P74F2Z
Dimension of a subspace 0QW084460E
Annihilator of a subspace 0R6M158SQ9
A linear isometry preserves the inner product 0R7VXTYHYZ
Dimension of a tensor product 0R84PF4JV7
A linear map is determined by its values on a basis 0R8X9XA83A
Bessel's inequality 0RBT5PB74K
Cauchy–Schwarz inequality 0RFWW56Y22
Projection 0RH4E3CAV9
Linear map 0RJF668P1T
Sum of subspaces 0RMKABS2S5
Trace of a linear map 0RPDTWY2JS
Linear form 0RT96J4D3H
Algebraic multiplicity 0S7A0EMPF4
Generalised eigenvector 0SAAHC36J9
Minor 0SD528P0EK
Multilinear map 0SDMPMCN43
Basis of a tensor product 0SH5VT8QYA
A space is the direct sum of a subspace and its orthogonal complement 0SP7P0G7KQ
Change of basis for a bilinear form 0SPYAGE7T0
Differentiation as a linear map 0SS770NS8B
Adjoint of a linear map 0ST8QF9T3T
Quotient space 0SVR29SV1V
Dimension of a quotient space 0SXDQ6TN00
Determinant is a coefficient of the characteristic polynomial 0T0X8GTYYS
Orthogonal vectors 0TS7VZJBWD
Symmetric bilinear form associated with a quadratic form 0TX2YH2FQS
Characteristic polynomial does not depend on the basis 0TYMASG33Y
Row rank equals column rank 0TZAG60ZYT
Intersection of subspaces 0V33SPH7RR
Minimal polynomial 0V58FPM3EQ
Determinant of a family of vectors in a basis 0V94H674MB
Special linear group 0V9PMN0RBH
Inner product 0VGSYBWHV2
Companion matrix 0VH1TC1PWF
Finite-dimensional spaces are isomorphic iff they have equal dimension 0VJBSK15SN
Cartan–Dieudonné theorem 0VMWGYY35Q
Space of linear maps 0VPCJWGMP9
Gram–Schmidt process 0VT6P0GNQR
Minimal polynomial divides every annihilating polynomial 0VTAD25A3G
Basis 0VTQTPQGAV
Cofactor 0W2QAVJQ1W
Sesquilinear form 0W44K2VNBD
Rank–nullity theorem 0W4FSW1TVB
Dual basis 0W6M3PSD08
Trace of a linear map is the trace of its matrix 0WCPH5Z7FA
Sylvester's law of inertia 0WFED3K3DQ
A subspace of full dimension is the whole space 0WGAXEK99E
Dimension theorem for vector spaces 0WK0Y8RH1M
Sylvester's criterion 0WKEF78PMV
Gram–Schmidt vectors are orthogonal 0WXBGBTA3D
Linear isomorphism 0XSJ25Z9M4
Existence of an orthonormal basis 0Y85GYEGSF
Distinct eigenvalues imply diagonalisable 0Y95Z7MT02
Universal property of the tensor product 0YDRV01R8F
Matrix of a linear map 0YYMY95FWS
Diagonalisation of a quadratic form 0Z3FEWZ8HA
Decomposition into generalised eigenspaces 0Z3GDY89T5
Determinant of the identity matrix 0Z4BWARC38
Dimension of the space of linear maps 0Z9N1ER0W0
Universal property of the quotient space 0ZERJX6PH6
Canonical isomorphism with the double dual 0ZJM9D7NPS
Determinant of a 2 by 2 matrix 0ZN2J42SK7
Eigenvalue 0ZND7NQ970
Matrix of the dual map is the transpose 0ZPB3180AY
Determinant of a transpose 0ZZQ2E1MTE

Sources

Web https://en.wikipedia.org/wiki/Vector_space, Definition and basic properties

What links here

Used by

External direct sum 02WZB422CE
Exterior algebra 08HK38GCSM
Norm 08NYZ2FS6B
Linear subspace 0EPTJA5QV4
Tensor product of vector spaces 0G31VJ5YS5
Quadratic form 0HZNE5QZDJ
Linear combination 0JB3DP1BMF
Product of vector spaces 0MM085RX00
Bilinear form 0P799D6AMN
Linear map 0RJF668P1T
Inner product 0VGSYBWHV2
Sesquilinear form 0W44K2VNBD