Commit 2025-04-29 08:58 072b045d

View on Github →

feat(NumberField): add ComplexEmbedding.lift (#24137) A (random) lift of a complex embedding φ : k →+* ℂ to an extension K of k.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Embeddings.lean

added theorem NumberField.ComplexEmbedding.lift_algebraMap_apply

added theorem NumberField.ComplexEmbedding.lift_comp_algebraMap

added theorem NumberField.InfinitePlace.comap_mk_lift