embeddings): some additional lemmas (#18473)

Commit

2 years ago

feat(number_theory/number_field/embeddings): some additional lemmas (#18473) Add some small lemmas that will be useful for other PRs.

Author

xroblot

Parents