Commit 2025-09-24 10:00 725b6fa8

View on Github →

chore: move NumberField/Completion.lean -> NumberField/InfinitePlace/Completion.lean (#29932) The file NumberField/Completion.lean contains the completion of a number field at an infinite place, so it is better placed in the InfinitePlace subdirectory. Also fix the following naming issues in Completion.lean

  • extensionEmbedding_of_isReal_coe -> extensionEmbeddingOfIsReal_coe
  • isometry_extensionEmbedding_of_isReal -> isometry_extensionEmbeddingOfIsReal
  • isClosed_image_extensionEmbedding_of_isReal -> isClosed_image_extensionEmbeddingOfIsReal
  • surjective_extensionEmbedding_of_isReal -> surjective_extensionEmbeddingOfIsReal
  • bijective_extensionEmbedding_of_isReal -> bijective_extensionEmbeddingOfIsReal

Estimated changes