Revision #2961 → #3489 · back to history
modifiedSVD related to polar decomposition27b91965e78b
| Field | From #2961 | To #3489 |
|---|
| note | The polar decomposition itself is not formalized in Mathlib, so its relation to the SVD is not formalized either. | Polar decomposition of operators/matrices is not present in Mathlib (loogle for "polarDecomposition" returns 0 hits), so its relation to the SVD is not formalized. |
modifiedConjugate transposece60eee613bc
| Field | From #2961 | To #3489 |
|---|
| mathlib.module | Mathlib.Data.Matrix.Basic | Mathlib.LinearAlgebra.Matrix.ConjTranspose |
| note | The conjugate transpose is defined on Mathlib matrices. | The conjugate transpose is defined on Mathlib matrices (Matrix.conjTranspose). |
addedEigendecomposition7e141b0e24ef
addedRectangular diagonal matrix83355ac8ead3
addedColumn spacec9dd8ac00b92
addedNull space (kernel)41b8ea7df429
addedPositive-semidefinite Hermitian matrix3923c118c4db
addedNormal matrix286407361130
addedMoore–Penrose pseudoinverse473434634f64
addedBidiagonal matrix33fcb813b71e
addedHouseholder reflection38e1ad47709f
addedQR decomposition076e4e23cb89
addedGivens rotation70dcd3dd072f
addedPauli matricesd78d3095627e
addedPartial isometry504b56193a9b
addedCompact operator81281669b4db
addedBorel functional calculusbe80e38beeda
addedSchatten p-norm030638da532b
addedOperator norm128b6b151605