I am maybe confused (the diff is a little hard to follow), but why removing place_conjugate (just to give an example)? Is it a special case of something more general?

I am maybe confused (the diff is a little hard to follow), but why removing place_conjugate (just to give an example)? Is it a special case of something more general?

Since this file became a big mess, especially everything concerning real embeddings, I decided to keep only what was needed for the proof of Dirichlet's theorem. It is possible that I went a bit too far. I'll see if I should put back some results that I deleted and I'll write a better PR description.

Thanks!

bors merge

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build
• Check all files imported
• Lint style