Mathlib Changelog
v4
Changelog
About
Github
Commit
2026-03-02 15:01
4aec2ac1
View on Github →
chore: move differential geometry elaborators tests into a separate directory (
#35891
)
Estimated changes
Renamed
MathlibTest/DifferentialGeometry/NotationAdvanced.lean
to
MathlibTest/DifferentialGeometry/Notation/Advanced.lean
Renamed
MathlibTest/DifferentialGeometry/Notation.lean
to
MathlibTest/DifferentialGeometry/Notation/Basic.lean
Renamed
MathlibTest/DifferentialGeometry/NotationSphere.lean
to
MathlibTest/DifferentialGeometry/Notation/Sphere.lean