Commit 2021-06-02 04:57 5a42f808

chore(logic/embedding): move some algebra content (#7776) This moves a lemma about multiplication by an element in a left/right cancellative semigroup being an embedding out of logic.embedding. I didn't find a great home for it, but put it with some content about regular elements, which is at least talking about similar mathematics. This removes the only direct import from the logic/ directory to the algebra/ directory. There are still indirect imports from logic.small, which currently brings in fintype and hence the whole algebra hierarchy. I'll look at that separately.