Revision #1316 → #2594 · back to history
modifiedCharacterization of inner products on R^n via symmetric positive-definite matrices73adaf525a72
| Field | From #1316 | To #2594 |
|---|
| mathlib.decl | Matrix.PosDef.toInnerProductSpace | Matrix.toInnerProductSpace |
| provenance | ai | ai-moderated |
modifiedHermitian form on complex coordinate space09f5d99e095c
| Field | From #1316 | To #2594 |
|---|
| mathlib.decl | Matrix.PosDef.toInnerProductSpace | Matrix.toInnerProductSpace |
| provenance | ai | ai-moderated |
modifiedOrthogonal vectors242e9aed2e87
| Field | From #1316 | To #2594 |
|---|
| mathlib.decl | Submodule.isOrtho | Submodule.IsOrtho |
| provenance | ai | ai-moderated |
modifiedPythagorean theorem for pairwise orthogonal vectorscda03e9ff86c
| Field | From #1316 | To #2594 |
|---|
| mathlib.decl | OrthogonalFamily.norm_sum_sq | OrthogonalFamily.norm_sum |
| provenance | ai | ai-moderated |
modifiedMazur–Ulam theorem for isometriesd158a39e7443
| Field | From #1316 | To #2594 |
|---|
| mathlib.decl | Isometric.toAffineIsometryEquiv | IsometryEquiv.toRealAffineIsometryEquiv |
| provenance | ai | ai-moderated |
modifiedSylvester's law of inertia9fde22c74b28
| Field | From #1316 | To #2594 |
|---|
| mathlib.decl | QuadraticForm.sigPos_eq_of_basis | QuadraticForm.sigPos_of_equiv_weightedSumSquares |
| provenance | ai | ai-moderated |