Commit 19f249b

committed

chore(Geometry/Manifold/MFDeriv/Basic): use custom elaborators (#40803)

As requested [here](#40748 (comment)).

1 parent 119eea4 commit 19f249bCopy full SHA for 19f249b

1 file changed

Mathlib/Geometry/Manifold/MFDeriv
- Basic.lean

Comments

(0)