Finite-dimensional vector spaces

AbbreviationFinite-dimensionality#

FiniteDimensional vector spaces are defined to be finite modules. Use Module.Basis.finiteDimensional_of_finite to prove finite dimension from another definition.

FiniteDimensional.{u_1, u_2} (K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V]
  [_root_.Module K V] : Prop
Sources
MathlibFiniteDimensional
Uses 4 · Used by 43
Statement usesFinite set · Generating sets · Rational number · Ring
Used byMinkowski’s Fundamental Theorem · Fourier transform as an integral · Inversion formula · Riemann-Lebesgue lemma (Analysis) · Lebesgue measure (Measures and integral calculus) · Approximation by convolution · Change of variables formula · Equivalence of norms in finite dimension · Finite-dimensional normed spaces over complete normed fields are complete · Heine-Borel theorem (finite-dimensional normed spaces are proper) · Galois correspondence · Category of finite-dimensional representations · Character · Nullstellensatz · Sphere · Diagonalization of self-adjoint endomorphisms · Existence of an eigenvalue · Primitive element theorem · Lie's theorem · Schur's lemma (1000+ theorems) · Rademacher's theorem · Fourier theorem · Helly's theorem · Whitney embedding theorem · Dirichlet's unit theorem · Lévy continuity theorem · Inscribed angle theorem · Decomposition of an orthogonal transformation as a product of reflections · Orthonormal bases · Adjoint endomorphism · Complex classification · Gram-Schmidt orthogonalisation · Sylvester's law of inertia (existence) · Sylvester's law of inertia (uniqueness) · Poisson’s formula · Convolution of two functions of \(\mathcal{S}(\R^d)\) · Fourier transforms on \(\mathcal{S}(\R^d)\) · Jordan-Chevalley-Dunford decomposition · Fourier transform on \(\mathrm{L}^2(\R^d)\) · Plancherel’s theorem · Riemann-Lebesgue lemma (Measures and integral calculus) · Continuity (continuity and differentiability of convex functions) · Riesz' lemma (unit-ball characterization of finite dimension)

DefinitionIsomorphism with \(K^n\)#

A module over R with a finite basis is linearly equivalent to functions from its basis to R.

Module.Basis.equivFun.{u_1, u_3, u_4} {ι : Type u_1} {R : Type u_3} {M : Type u_4} [Semiring R]
  [AddCommMonoid M] [_root_.Module R M] [Finite ι] (b : Module.Basis ι R M) : M ≃ₗ[R] ι → R
Sources
MathlibModule.Basis.equivFun
Uses 1 · Used by 7
Statement usesBasis
Used byFinite-dimensional normed spaces over complete normed fields are complete · Matrix representation · Diagonalization of self-adjoint endomorphisms · Matrix representation of a linear map · Rademacher's theorem · Inscribed angle theorem · Sylvester's law of inertia (existence)

DefinitionIsomorphism with bidual#

The bijection between a reflexive module and its double dual, bundled as a LinearEquiv.

Module.evalEquiv.{u_1, u_2} (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M]
  [_root_.Module R M] [Module.IsReflexive R M] : M ≃ₗ[R] Module.Dual R (Module.Dual R M)
Sources
MathlibModule.evalEquiv
Uses 2
Statement usesDual vector space · Range of a linear map

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.