Skip to content

[Merged by Bors] - feat: custom elaborators for TangentSpace and tangentMap(Within)#36155

Closed
grunweg wants to merge 16 commits into
leanprover-community:masterfrom
grunweg:tangentspace-elaborators
Closed

[Merged by Bors] - feat: custom elaborators for TangentSpace and tangentMap(Within)#36155
grunweg wants to merge 16 commits into
leanprover-community:masterfrom
grunweg:tangentspace-elaborators

Commits

Commits on May 27, 2026

Commits on May 30, 2026

Commits on May 31, 2026

Commits on Jun 3, 2026

Commits on Jun 5, 2026

Commits on Jun 14, 2026