WikiLean Articles · Brain · Recent changes · Proposals · Flags · Stats · About

Diff — Basis (linear algebra)

Revision #1030 → #2459 · back to history

modifiedBasis (informal)3433a4a87dce
FieldFrom #1030To #2459
mathlib.decl—Module.Basis
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Module.Basis ι R M is Mathlib's ι-indexed basis of a module M, packaged as a linear equivalence M ≃ₗ[R] (ι →₀ R).
status—formalized
modifiedBasis as linearly independent spanning set3e1a98afef89
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.mk
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Basic
note—Basis.mk constructs a Basis from a family v satisfying LinearIndependent v and span R (range v) = ⊤.
status—formalized
modifiedAll bases have the same cardinality (dimension)ec935c147d52
FieldFrom #1030To #2459
mathlib.decl—mk_eq_mk_of_basis
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dimension.StrongRankCondition
note—mk_eq_mk_of_basis states that any two bases of the same module over a strong-rank-condition ring have equal cardinality.
status—formalized
modifiedBasis of a vector space over a field12f81b0b435f
FieldFrom #1030To #2459
mathlib.decl—Module.Basis
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Module.Basis is defined over any semiring, specialising to bases of vector spaces when R is a field.
status—formalized
modifiedLinear independence condition312e69f827ee
FieldFrom #1030To #2459
mathlib.decl—LinearIndependent
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.LinearIndependent.Defs
note—LinearIndependent R v captures the finite-sum condition via injectivity of the linear combination map.
status—formalized
modifiedSpanning propertydfda82eda558
FieldFrom #1030To #2459
mathlib.decl—Submodule.span
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Span.Defs
note—The spanning condition is the standard Mathlib statement Submodule.span R S = ⊤ using Submodule.span.
status—formalized
modifiedEquivalent phrasing of linear independence6712e268a4bb
FieldFrom #1030To #2459
mathlib.decl—linearIndependent_iff_notMem_span
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.LinearIndependent.Defs
note—linearIndependent_iff_notMem_span is one of several equivalent characterisations of LinearIndependent.
status—formalized
modifiedUnique representation in a basisc85145cd3f82
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.linearCombination_repr
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Basis.repr is itself the linear equivalence M ≃ₗ ι →₀ R, and linearCombination_repr shows the coordinates recompose x uniquely.
status—formalized
modifiedFinite-dimensional vector space845fdfb2c2c4
FieldFrom #1030To #2459
mathlib.decl—FiniteDimensional
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.FiniteDimensional.Defs
note—FiniteDimensional K V (abbrev for Module.Finite) is Mathlib's finite-dimensionality predicate.
status—formalized
modifiedOrdered basis972c57f4e321
FieldFrom #1030To #2459
mathlib.decl—Module.Basis
mathlib.match_kind—generalization
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Mathlib's Basis is inherently indexed by a type ι, so it corresponds directly to an ordered basis when ι is Fin n or another ordered index.
status—formalized
modifiedStandard basis of R^278b4d9df119e
FieldFrom #1030To #2459
mathlib.decl—Pi.basisFun
mathlib.match_kind—invocation
mathlib.module—Mathlib.LinearAlgebra.StdBasis
note—Pi.basisFun R (Fin 2) is the standard basis of Fin 2 → R, i.e. the (1,0),(0,1) basis of R².
status—formalized
modifiedStandard basis of F^n9141626a02ef
FieldFrom #1030To #2459
mathlib.decl—Pi.basisFun
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.StdBasis
note—Pi.basisFun R η gives the standard basis on η → R with basis vectors Pi.single i 1.
status—formalized
modifiedMonomial basis of F[X]765950849080
FieldFrom #1030To #2459
mathlib.decl—MvPolynomial.basisMonomials
mathlib.match_kind—generalization
mathlib.module—Mathlib.RingTheory.MvPolynomial.Basic
note—MvPolynomial.basisMonomials is the monomial basis for multivariate polynomials; the univariate case (X^i basis of R[X]) is not called out under its own name.
status—partial
modifiedPolynomial sequence basis69e2c633f3c0
FieldFrom #1030To #2459
mathlib.decl—Polynomial.Sequence.basis
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Polynomial.Sequence
note—Polynomial.Sequence.basis turns any polynomial sequence with one polynomial of each degree into a basis of R[X].
status—formalized
modifiedSteinitz exchange lemma55fb74bbd56d
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.extend
mathlib.match_kind—invocation
mathlib.module—Mathlib.LinearAlgebra.Basis.VectorSpace
note—The Steinitz exchange lemma is not stated under that name; its usual consequences (extending an independent set to a basis, invariance of dimension) are present via Basis.extend and mk_eq_mk_of_basis.
status—partial
modifiedExtending an independent set to a basis461fe2e12e0e
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.extend
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.VectorSpace
note—Basis.extend extends any LinearIndepOn set to a basis of V.
status—formalized
modifiedEvery vector space has a basis0326797cbe12
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.ofVectorSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.VectorSpace
note—Basis.ofVectorSpace produces a basis of any vector space V over a division ring K.
status—formalized
modifiedDimension theorem38a007473f68
FieldFrom #1030To #2459
mathlib.decl—mk_eq_mk_of_basis
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dimension.StrongRankCondition
note—mk_eq_mk_of_basis is Mathlib's dimension theorem: any two bases have equal cardinality.
status—formalized
modifiedBasis as minimal generating set7a50fb978059
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No direct 'basis iff minimal spanning set' characterisation found in Mathlib.
status—not_formalized
modifiedBasis as maximal independent set01415c44c52d
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.maximal
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Basic
note—Basis.maximal shows any basis is a maximal linearly independent family (over a nontrivial semiring).
status—formalized
modifiedn-element independent subset is a basisfd7494aea9b8
FieldFrom #1030To #2459
mathlib.decl—basisOfLinearIndependentOfCardEqFinrank
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
note—basisOfLinearIndependentOfCardEqFinrank turns a linearly independent family of size finrank K V into a basis.
status—formalized
modifiedn-element spanning subset is a basis33323e42b679
FieldFrom #1030To #2459
mathlib.decl—basisOfTopLeSpanOfCardEqFinrank
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Dimension.OrzechProperty
note—basisOfTopLeSpanOfCardEqFinrank turns a spanning family of size finrank K V into a basis.
status—formalized
modifiedCoordinates over a basis0c87902bb128
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.coord
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Basis.coord i v gives the i-th coordinate of v over the basis; the whole coordinate vector is Basis.repr.
status—formalized
modifiedCoordinate isomorphism3504bcf98764
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.equivFun
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Basis.equivFun b : M ≃ₗ[R] ι → R is the coordinate isomorphism for finite ι (with Basis.repr for the general Finsupp version).
status—formalized
modifiedStandard/canonical basis of F^nac28ccea004c
FieldFrom #1030To #2459
mathlib.decl—Pi.basisFun
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.StdBasis
note—Pi.basisFun R η is Mathlib's standard/canonical basis on η → R.
status—formalized
modifiedOrdered bases correspond to linear isomorphisms396922662539
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.equivFun
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—By definition a Basis is a linear equiv M ≃ₗ[R] (ι →₀ R); Basis.equivFun/Basis.ofEquivFun witnesses the correspondence with linear isos to R^n.
status—formalized
modifiedChange-of-basis formula172246dee3fb
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.toMatrix
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Matrix.Basis
note—Basis.toMatrix records the coordinates of one basis in another and is used to state the change-of-basis formula.
status—formalized
modifiedMatrix form of change of basis2bb0b6a95ece
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.toMatrix_mul_toMatrix
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Matrix.Basis
note—Basis.toMatrix_mul_toMatrix expresses the composition law of change-of-basis matrices.
status—formalized
modifiedModule897843739c9f
FieldFrom #1030To #2459
mathlib.decl—Module
mathlib.match_kind—exact
mathlib.module—Mathlib.Algebra.Module.Defs
note—Module R M is Mathlib's typeclass for a module over a semiring/ring R.
status—formalized
modifiedFree module54495097b8d7
FieldFrom #1030To #2459
mathlib.decl—Module.Free
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.FreeModule.Basic
note—Module.Free R M asserts M has a basis; Module.Free.exists_basis produces one.
status—formalized
addedNot every module has a basis673f17bcea25
modifiedSubgroup of a free abelian group is freed22a9cd78468
FieldFrom #1030To #2459
labelSubgroup of finitely generated free abelian groupSubgroup of a free abelian group is free
mathlib.decl—Submodule.basisOfPid
mathlib.match_kind—special_case
mathlib.module—Mathlib.LinearAlgebra.FreeModule.PID
note—Submodule.basisOfPid gives a basis for a finitely generated submodule of a free module over a PID; specialised to R=ℤ this yields freeness of finitely generated subgroups of free abelian groups, but the fully general (arbitrary rank) statement isn't stated directly under that name.
provenanceai-agent1ai-moderated
status—partial
modifiedHamel basis7c256dcb11a0
FieldFrom #1030To #2459
mathlib.decl—Module.Basis
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.Defs
note—Mathlib's Module.Basis is a Hamel (algebraic) basis by default; the term 'Hamel' is not used in the library name but the concept coincides.
status—formalized
modifiedCardinality of Hamel basis of R over Qe8e255802bb9
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No Mathlib statement identifying the cardinality of a ℚ-basis of ℝ with the continuum.
status—not_formalized
modifiedHamel basis of a Banach space is uncountable3974a566f34c
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Baire-category argument giving uncountability of Hamel bases of infinite-dimensional Banach spaces is not present under any name I could find.
status—not_formalized
modifiedCountable Hamel basis of finitely-supported sequences45f0fe80b0bb
FieldFrom #1030To #2459
mathlib.decl—Finsupp.basisSingleOne
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Finsupp.VectorSpace
note—The space of finitely supported sequences is (ι →₀ R), and Finsupp.basisSingleOne is its standard basis of single-support vectors.
status—formalized
modifiedOrthogonal Fourier basis of square-integrable functionsb4ed680baf92
FieldFrom #1030To #2459
mathlib.decl—fourierBasis
mathlib.match_kind—exact
mathlib.module—Mathlib.Analysis.Fourier.AddCircle
note—fourierBasis is Mathlib's HilbertBasis of Lp ℂ 2 haarAddCircle built from the Fourier characters.
status—formalized
modifiedFourier basis is not a Hamel basis00dcc7b0f014
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The remark that the Fourier basis is not a Hamel basis is an informal aside without a corresponding Mathlib lemma.
status—not_formalized
modifiedAffine basisb09a02604de7
FieldFrom #1030To #2459
mathlib.decl—AffineBasis
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.AffineSpace.Basis
note—AffineBasis ι k P is Mathlib's structure for an affine basis of an affine space.
status—formalized
modifiedProjective basis566a83d32b0f
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No 'projective basis' (frame of n+2 points in general position) definition found in Mathlib's Projectivization files.
status—not_formalized
modifiedConvex basis381791e3896a
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Mathlib has convex hulls and extreme points but does not name a 'convex basis of a polytope' as such.
status—not_formalized
modifiedCone basisdbc3b0736362
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—No definition of a 'cone basis' (minimal set of generators of a polyhedral cone) present in Mathlib.
status—not_formalized
modifiedRandom vectors form a basis with probability one6db9a104c63b
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The probabilistic statement about n random vectors is not formalised in Mathlib.
status—not_formalized
modifiedε-orthogonalityd8a1c716662a
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The quantitative ε-orthogonality condition |⟨x,y⟩| ≤ ε‖x‖‖y‖ is not a named notion in Mathlib.
status—not_formalized
modifiedExponential growth of almost-orthogonal random vectors7581ce329830
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—Concentration-of-measure style result about pairwise ε-orthogonal random vectors is not present.
status—not_formalized
modifiedEvery vector space has a basis (proof via Zorn)a2014fb0315b
FieldFrom #1030To #2459
mathlib.decl—Module.Basis.ofVectorSpace
mathlib.match_kind—exact
mathlib.module—Mathlib.LinearAlgebra.Basis.VectorSpace
note—Basis.ofVectorSpace is Mathlib's Zorn-based existence-of-basis construction for any vector space over a division ring.
status—formalized
modifiedExistence of bases equivalent to axiom of choice10edbefeb7af
FieldFrom #1030To #2459
mathlib.decl——
mathlib.match_kind——
mathlib.module——
note—The Blass converse ('every vector space has a basis' ⇒ AC) is not formalised in Mathlib.
status—not_formalized