mathlib
f29120f8
- chore(order/rel_iso/basic): better `namespace` management (#18758)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
chore(order/rel_iso/basic): better `namespace` management (#18758) We remove a lot of `_root_` by simply closing and reopening a namespace.
Author
vihdzp
Parents
dc65937e
Loading