Commit 2024-12-07 04:52 cc6b7b9d

View on Github →

chore(Mathlib/NumberTheory/NumberField/*): rename completion -> Completion (#19646) We have UniformSpace.Completion so it should surely also be AbsoluteValue.Completion v : Type* and NumberField.InfinitePlace.Completion v : Type* (currently they are both completion and both types).

Estimated changes

Modified Mathlib/Analysis/Normed/Ring/WithAbs.lean

modified theorem AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

modified def NumberField.InfiniteAdeleRing

Modified Mathlib/NumberTheory/NumberField/Completion.lean

modified def NumberField.InfinitePlace.Completion.extensionEmbedding

modified def NumberField.InfinitePlace.Completion.extensionEmbedding_of_isReal

modified def NumberField.InfinitePlace.Completion.isometryEquiv_real_of_isReal

modified def NumberField.InfinitePlace.Completion.ringEquiv_real_of_isReal