Commit 2024-11-08 12:39 2b878991

View on Github →

feat: the completion of a number field at an infinite place (#16483) This PR contains the following:

The completion NumberField.InfinitePlace.completion of a number field at an infinite place, which is derived from AbsoluteValue.completion as InfinitePlace is a subtype of AbsoluteValue.
Proofs that if an infinite place of a number field is real/complex then the resultant completion is isomorphic to the real/complex numbers. cf. #13577 for previous feedback

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Field/Subfield.lean

added theorem RingHom.fieldRange_eq_top_iff

added theorem RingHom.mem_fieldRange_self

Created Mathlib/NumberTheory/NumberField/Completion.lean

added theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isComplex

added theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isReal

added def NumberField.InfinitePlace.Completion.extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.extensionEmbedding_coe

added def NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal

added theorem NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal_coe

added theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding_of_isReal

added def NumberField.InfinitePlace.Completion.isometryEquiv_complex_of_isComplex

added def NumberField.InfinitePlace.Completion.isometryEquiv_real_of_isReal

added theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbedding_of_isReal

added def NumberField.InfinitePlace.Completion.ringEquiv_complex_of_isComplex

added def NumberField.InfinitePlace.Completion.ringEquiv_real_of_isReal

added theorem NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex

added theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex

added theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isReal