You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If I click on a declaration in the blueprint graph, can we discretely have at the bottom of the pop-up window LaTeX: ZHat.torsionFree ; Lean: ZHat.torsionFree or something like that, so I can cut and paste labels?
The text was updated successfully, but these errors were encountered:
If I click on a declaration in the blueprint graph, can we discretely have at the bottom of the pop-up window
LaTeX: ZHat.torsionFree ; Lean: ZHat.torsionFree
or something like that, so I can cut and paste labels?The text was updated successfully, but these errors were encountered: