Revision #1172 → #2560 · back to history
modifiedDual setd65020828e65
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis | Module.Basis.dualBasis |
| provenance | ai | ai-moderated |
modifiedDual set is a basis when finite-dimensional7e436a4b1c14
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis | Module.Basis.dualBasis |
| provenance | ai | ai-moderated |
modifiedDual basis (finite-dimensional)41735d4ff9d0
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis | Module.Basis.dualBasis |
| provenance | ai | ai-moderated |
modifiedBi-orthogonality property932adb08a507
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis_apply_self | Module.Basis.dualBasis_apply_self |
| provenance | ai | ai-moderated |
modifiedMatrix biorthogonality of basis and dual basisfc077aacb3f1
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis_apply_self | Module.Basis.dualBasis_apply_self |
| provenance | ai | ai-moderated |
modifiedInfinite-dimensional dual: independent but not a basis671a4272d3ee
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis | Module.Basis.dualBasis |
| provenance | ai | ai-moderated |
modifiedDual identified with function space on a basis25edd2ff9b0b
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.dualBasis | Module.Basis.dualBasis |
| provenance | ai | ai-moderated |
modifiedDual of infinite-dimensional space has larger dimension354ee36ab5aa
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Module.lift_rank_lt_rank_dual | lift_rank_lt_rank_dual |
| provenance | ai | ai-moderated |
modifiedErdős–Kaplansky theoreme7ae04001119
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Module.rank_dual_eq_card_dual_of_aleph0_le_rank | rank_dual_eq_card_dual_of_aleph0_le_rank |
| provenance | ai | ai-moderated |
modifiedV isomorphic to V* but not naturally70ff018e7fc9
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Basis.toDualEquiv | Module.Basis.toDualEquiv |
| provenance | ai | ai-moderated |
modifiedDouble annihilator and Galois connection (finite-dim)0454ae75fbe7
| Field | From #1172 | To #2560 |
|---|
| mathlib.decl | Module.dualAnnihilator_gc | Submodule.dualAnnihilator_gc |
| provenance | ai | ai-moderated |