Revision #3435 → #4002 · back to history
modifiedSteinitz exchange lemma55fb74bbd56d
| Field | From #3435 | To #4002 |
|---|
| mathlib.decl | Module.Basis.extend | exists_of_linearIndepOn_of_finite_span |
| mathlib.match_kind | invocation | exact |
| mathlib.module | Mathlib.LinearAlgebra.Basis.VectorSpace | Mathlib.LinearAlgebra.LinearIndependent.Lemmas |
| 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. | exists_of_linearIndepOn_of_finite_span is the Steinitz exchange lemma: any linearly independent set in the span of a finite set t can be extended within s ∪ t to a set of the same cardinality as t. |
| status | partial | formalized |
modifiedBasis as minimal generating set7a50fb978059
| Field | From #3435 | To #4002 |
|---|
| note | No direct 'basis iff minimal spanning set' characterisation found in Mathlib. | No direct 'basis iff minimal spanning set' characterisation for modules found in Mathlib (the analogous statement exists for matroids, not linear algebra). |
modifiedCardinality of Hamel basis of R over Qe8e255802bb9
| Field | From #3435 | To #4002 |
|---|
| mathlib.decl | — | Real.rank_rat_real |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.LinearAlgebra.Complex.FiniteDimensional |
| note | No Mathlib statement identifying the cardinality of a ℚ-basis of ℝ with the continuum. | Real.rank_rat_real states Module.rank ℚ ℝ = Cardinal.continuum, i.e. any ℚ-basis of ℝ has continuum cardinality. |
| status | not_formalized | formalized |
addedLinear combinationa90ffab76aca
addedZorn's lemma07739b2dc2b5
addedCoordinate vectorb4321c90b6f0