Revision #3187 → #3688 · back to history
modifiedHodge star operator5e07b2cd8fc9
| Field | From #3187 | To #3688 |
|---|
| note | No Hodge star operator is defined anywhere in Mathlib4 (no `hodgeStar`/`Hodge` results in `Mathlib/`). | Grep for `Hodge`, `hodgeStar`, `HodgeStar` in `Mathlib/` returns no definition of a Hodge star operator. |
modifiedCodifferential (lead)2f4fd6a0430d
| Field | From #3187 | To #3688 |
|---|
| note | The codifferential as Hodge-adjoint of the exterior derivative is not defined in Mathlib. | No `codifferential` decl exists in Mathlib and no Hodge-adjoint of the exterior derivative is defined. |
modifiedLaplace–de Rham operator (lead)4b8d7db43fd3
| Field | From #3187 | To #3688 |
|---|
| note | The Laplace–de Rham (Hodge) Laplacian is not formalized in Mathlib. | No `LaplaceRham`/`HodgeLaplacian`/`deRham` Laplacian appears in Mathlib. |
modifiedInduced inner product on k-vectorsc7e46dcc6439
| Field | From #3187 | To #3688 |
|---|
| mathlib.decl | — | exteriorPower.inner_ιMulti_ιMulti |
| mathlib.match_kind | — | exact |
| mathlib.module | — | Mathlib.Analysis.InnerProductSpace.ExteriorPower |
| note | Mathlib has `ExteriorPower` and inner product spaces but no induced inner product on the exterior power of an inner product space. | `Mathlib.Analysis.InnerProductSpace.ExteriorPower` builds an `InnerProductSpace ℝ (⋀[ℝ]^n E)` instance with `inner_ιMulti_ιMulti` giving exactly the Gram determinant formula on decomposables. |
| status | not_formalized | formalized |
addedHodge star maps k-vectors to (n−k)-vectors7315ec1d97ed
addedGram matrix of an inner product on k-vectors7f5b62d544b2
addedHodge star on 2-forms in Minkowski space06ab21d2a28a