mathlib3
refactor(topology/dense_embedding): move dense embeddings to new file
#1515
Merged
Merged
refactor(topology/dense_embedding): move dense embeddings to new file #1515
mergify
merged
2 commits into
master
from
rwbarton-top4
refactor(topology/dense_embedding): move dense embeddings to new file
f694f4f6
jcommelin
commented
on 2019-10-07
PatrickMassot
approved these changes
on 2019-10-07
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into rwbarton-top4
c0ea51c7
Reviewers
Assignees
No one assigned
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub