Theorem VectorField.mlieBracket_const_smul_left

Modification history

2026-03-02 18:03

Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

chore(Manifold/VectorBundle/LieBracket): golf using custom elaborators (#35729)

Modified VectorField.mlieBracket_const_smul_left View on Github →

2025-07-04 10:05

Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

feat(Analysis/Calculus/VectorField): Implement product rule for liebrackets (#26725) …

Added VectorField.mlieBracket_const_smul_left View on Github →