Revision #3200 → #3705 · back to history
modifiedGram–Schmidt processe21b7c0b0e10
| Field | From #3200 | To #3705 |
|---|
| mathlib.decl | gramSchmidt | InnerProductSpace.gramSchmidt |
| note | `gramSchmidt 𝕜 f` produces the orthogonal sequence from a linearly independent one; `gramSchmidtNormed` gives the orthonormal version. | `InnerProductSpace.gramSchmidt 𝕜 f` produces the orthogonal sequence from a linearly independent one; `InnerProductSpace.gramSchmidtNormed` gives the orthonormal version. |
modifiedOrthogonal projection onto a subspacec6552fcf908b
| Field | From #3200 | To #3705 |
|---|
| mathlib.decl | orthogonalProjectionOnto | Submodule.orthogonalProjectionOnto |
| note | `Submodule.orthogonalProjectionOnto K` (with legacy alias `orthogonalProjection`) is the continuous linear projection of a Hilbert space onto a complete subspace `K`. | `Submodule.orthogonalProjectionOnto K` (alias of `Submodule.orthogonalProjection`) is the continuous linear projection of a Hilbert space onto a complete subspace `K`. |
modifiedContinuous linear maps between inner product spaces7a3fc2241aec
| Field | From #3200 | To #3705 |
|---|
| mathlib.module | Mathlib.Topology.Algebra.Module.Basic | Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic |
modifiedNondegenerate conjugate symmetric formfd777bf45f81
| Field | From #3200 | To #3705 |
|---|
| mathlib.module | Mathlib.LinearAlgebra.BilinearForm.Basic | Mathlib.LinearAlgebra.BilinearForm.Properties |
addedRiemannian manifold34f82d27728e
addedOuter product of vector and covector5bf424d3988c
addedExterior/wedge product8cd2cb4426de
addedClifford algebra / geometric product6c71c9ab66b1