mathlib
3484194d - chore(geometry/manifold/real_instance): remove global fact instance (#3549)

Commit
5 years ago
chore(geometry/manifold/real_instance): remove global fact instance (#3549) Remove global `fact` instance that was used to get a manifold structure on `[0, 1]`, and register only the manifold structure.
Author
Parents
Loading