Commit 2025-09-19 09:10 ba68f6f7

feat: predicates for extensions of complex embeddings (#27977) If L/K and ψ : K →+* ℂ, we define the subtype ComplexExtension L ψ of L →+* ℂ that extend ψ to L. Also define two predicates asserting ways that φ can extend ψ.

• φ.IsMixed : ψ has real image while φ has complex image.
• φ.IsUnmixed: the negation of IsMixed -- ψ has real image if and only if φ has real image. ComplexExtension.IsMixed and ComplexExtension.IsUnmixed are the ComplexEmbedding analogues to ramified and unramified infinite places, which is a two-to-one isomorphism in the former and a one-to-one isomorphism in the latter, hence the slightly different terminology. This PR continues the work from #24877. Original PR: https://github.com/leanprover-community/mathlib4/pull/24877