Theorem mulInvariantVectorField_eq_mpullback

Modification history

2026-06-15 11:33
Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
feat: custom elaborators for TangentSpace and tangentMap(Within) (#36155) …
Modified mulInvariantVectorField_eq_mpullbackView on Github →
2025-04-11 13:45
Mathlib/Geometry/Manifold/GroupLieAlgebra.lean
feat: the Lie algebra of a Lie group over a general field (#18396) …
Added mulInvariantVectorField_eq_mpullbackView on Github →