Finite-dimensional vector space

Constructively, a $𝕂$ -vector space $𝑉$ has dimension $𝑛$ if there merely exists an isomorphism $𝑉 ≅ 𝕂 𝕂 𝑛$ , i.e. $𝑉$ is $𝑛$ -framable. #m/def/linalg Thus a finite-dimensional vector space $𝑉$ is equipped with an $𝑛$ such that $𝑉$ is $𝑛$ -dimensional, i.e. an element of

∐ 𝑛 \in ℕ ‖ 𝑉 ≅ 𝕂 𝕂 𝑛 ‖ .

#state/tidy | #lang/en | #SemBr