Commit 2025-05-05 07:39 abf6080f

chore(NumberField): split embeddings.lean (#24478) The file NumberTheory.NumberField.Embeddings is getting a bit long (around 1250 lines), so this PR splits it into 4 files:

• InfinitePlace.Embeddings: results about complex embeddings
• InfinitePlace.Basic: definitions and first results about infinite places
• InfinitePlace.Ramification: ramification of infinite places in extensions
• InfinitePlace.TotallyRealComplex: stuff about totally real and totally complex number fields. The docs of the four files have been extended to include more definitions and results.