Commit 2019-09-18 17:59 066d0535
View on Github →chore(topology/maps): a few tweaks to open_embedding and closed embeddings (#1459)
- chore(topology/maps): a few tweaks to open_embedding and closed embeddings aligning them with recent modification to embedding. From the perfectoid project.
- chore(topology/maps): add missing empty line