---
tag: 05G2G0P224
kind: definition
name: Dimension
msc: [15A03]
defines: 03GSZ8RTZJ
uses: [0VTQTPQGAV, 018W3V3TCT]
sources:
  - url: https://en.wikipedia.org/wiki/Dimension_(vector_space)
    locator: lead section
---

## Definition

Let $F$ be a field and let $V$ be a [[finite-dimensional|0ZHWKQMVX5]] vector space over $F$.
The *dimension* of $V$ over $F$, written $\dim_F V$ or $\dim V$, is the number of vectors in a [[basis|0KCQ9Y3QKA]] of $V$.
For an arbitrary vector space, the dimension is the cardinality of a basis.

## Remarks

The number is well defined, by the [[dimension theorem for vector spaces|0WK0Y8RH1M]].
The zero space $\{0\}$ has the empty basis and dimension $0$.
The dimension depends on the field: $\dim_\C \C = 1$, but $\dim_\R \C = 2$.
Mathlib writes `Module.finrank F V` for the dimension as a natural number, with value $0$ for infinite-dimensional spaces.

## Explanations

### L1 human

The dimension counts the independent directions in a space.
A line has dimension $1$, a plane has dimension $2$, and ordinary space has dimension $3$.
Every basis of a space has this same number of vectors.