Revision #1925 → #2667 · back to history
modifiedEvery vector space has a basis2d888fb42a2b
| Field | From #1925 | To #2667 |
|---|
| mathlib.decl | exists_basis | Module.Basis.exists_basis |
| provenance | ai | ai-moderated |
modifiedCoordinates on a basis8c863bb13e67
| Field | From #1925 | To #2667 |
|---|
| mathlib.decl | Basis.repr | Module.Basis.repr |
| provenance | ai | ai-moderated |
modifiedCoordinate map is an isomorphismd7a9c55c7bf6
| Field | From #1925 | To #2667 |
|---|
| mathlib.decl | Basis.repr | Module.Basis.repr |
| provenance | ai | ai-moderated |
modifiedOrdered pairs of numbers75f8799262fe
| Field | From #1925 | To #2667 |
|---|
| mathlib.decl | Prod.module | Prod.instModule |
| provenance | ai | ai-moderated |
modifiedClassification of vector spaces by dimension3caecc7dc819
| Field | From #1925 | To #2667 |
|---|
| mathlib.decl | nonempty_linearEquiv_of_finrank_eq | FiniteDimensional.nonempty_linearEquiv_of_finrank_eq |
| provenance | ai | ai-moderated |
modifiedQuotient vector spaceb95cfefe2e53
| Field | From #1925 | To #2667 |
|---|
| mathlib.decl | Submodule.Quotient | Submodule.hasQuotient |
| provenance | ai | ai-moderated |