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