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.
