Finite-dimensional vector spaces

• Finite-dimensionality
• Isomorphism with \(K^n\)

AbbreviationRank of a linear map#

rank f is the rank of a LinearMap f, defined as the dimension of f.range.

LinearMap.rank.{u, v, v'} {K : Type u} {V : Type v} {V' : Type v'} [Semiring K] [AddCommMonoid V]
  [_root_.Module K V] [AddCommMonoid V'] [_root_.Module K V'] (f : V →ₗ[K] V') : Cardinal.{v'}

Sources

• Mathlib documentation: LinearMap.rank
• Source of LinearMap.rank in Mathlib/LinearAlgebra/Dimension/LinearMap.lean
• Mathlib undergraduate list: Linear algebra › Finite-dimensional vector spaces

MathlibLinearMap.rank

Uses 3

Statement usesCardinal · Linear independence · Range of a linear map

DefinitionRank of a set of vectors#

The rank of a set of vectors as a natural number.

Set.finrank.{u, v} (R : Type u) {M : Type v} [Semiring R] [AddCommMonoid M] [_root_.Module R M]
  (s : Set M) : ℕ

Sources

• Mathlib documentation: Set.finrank
• Source of Set.finrank in Mathlib/LinearAlgebra/Dimension/Constructions.lean
• Mathlib undergraduate list: Linear algebra › Finite-dimensional vector spaces

MathlibSet.finrank

Uses 3

Statement usesCardinal · Generating sets · Linear independence

• Isomorphism with bidual

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.