Revision #3483 → #4050 · back to history
modifiedLie derivative57f491bcd6d7
| Field | From #3483 | To #4050 |
|---|
| mathlib.decl | — | VectorField.mlieBracket |
| mathlib.match_kind | — | special_case |
| mathlib.module | — | Mathlib.Geometry.Manifold.VectorField.LieBracket |
| note | Lie derivatives on smooth manifolds are not currently formalized in Mathlib at this level of generality. | Mathlib formalizes the Lie bracket of vector fields on manifolds (`VectorField.mlieBracket`, coinciding with the Lie derivative of a vector field along another), but the general Lie derivative acting on tensors/forms is not yet formalized. |
| status | not_formalized | partial |
modifiedInverse Laplace transformd9607b5108f4
| Field | From #3483 | To #4050 |
|---|
| note | The Laplace transform and its inverse are not formalized in Mathlib. | The Laplace transform and its inverse are not formalized in Mathlib (only Mellin and Fourier transforms are). |
modifiedHankel function of the first kindf94660b5ad34
| Field | From #3483 | To #4050 |
|---|
| note | Hankel functions are not formalized in Mathlib. | Hankel functions (and Bessel functions more generally) are not formalized in Mathlib. |