Commit 2026-03-02 18:03 e4c544d9

View on Github →

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

Estimated changes

Modified Mathlib/Geometry/Manifold/VectorField/LieBracket.lean

modified theorem VectorField.mlieBracket_add_left

modified theorem VectorField.mlieBracket_add_right

modified theorem VectorField.mlieBracket_const_smul_left

modified theorem VectorField.mlieBracket_const_smul_right