Commit 2025-04-11 13:45 28daac21

feat: the Lie algebra of a Lie group over a general field (#18396) We construct the Lie algebra of a Lie group, where the bracket is given by the vector field bracket of invariant vector fields associated to an element of the Lie algebra, i.e., the tangent space at the identity. The Jacobi identity follows from the fact that it is satisfied generally by the Lie bracket of vector fields. Our construction of the Lie algebra of a Lie group makes sense when the Lie group is C^n for n = minSmoothness 𝕜 3, i.e., C^3 over the reals or the complexes, analytic otherwise. This ensures symmetry of second derivatives, which is needed for the Jacobi identity.