Revision #2368 → #2602 · back to history
modifiedBasis between independent and spanning setse36e6e62bf60
| Field | From #2368 | To #2602 |
|---|
| mathlib.decl | Basis.extend | Module.Basis.extend |
| provenance | ai | ai-moderated |
modifiedCoordinate isomorphism from a basis52cdb0408711
| Field | From #2368 | To #2602 |
|---|
| mathlib.decl | Basis.equivFun | Module.Basis.equivFun |
| provenance | ai | ai-moderated |
modifiedCoordinate vector / column matrix4c5cde2fb540
| Field | From #2368 | To #2602 |
|---|
| mathlib.decl | Basis.repr | Module.Basis.repr |
| provenance | ai | ai-moderated |
modifiedDual basis8d3191f8684d
| Field | From #2368 | To #2602 |
|---|
| mathlib.decl | Basis.dualBasis | Module.Basis.dualBasis |
| provenance | ai | ai-moderated |
modifiedGram–Schmidt procedure1f37467d2d9d
| Field | From #2368 | To #2602 |
|---|
| mathlib.decl | gramSchmidtOrthonormalBasis | InnerProductSpace.gramSchmidtOrthonormalBasis |
| provenance | ai | ai-moderated |
modifiedEvery module is a cokernel of free modules068ada34926f
| Field | From #2368 | To #2602 |
|---|
| mathlib.decl | Module.tautologicalRelations | Module.Presentation.tautologicalRelations |
| provenance | ai | ai-moderated |