Commit 2026-10-30 13:18 9756d93f

View on Github →

refactor: make AbsoluteValue.Completion a one-field structure (#45407) See InfinitePlace.Completion and WithLp for analogous library implementations of one-field structures. Afterwards InfinitePlace.Completion will become an abbrev.

Estimated changes

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

deleted theorem AbsoluteValue.Completion.algebraMap_apply

added theorem AbsoluteValue.Completion.algebraMap_apply_of_liesOver

added theorem AbsoluteValue.Completion.algebraMap_def

deleted theorem AbsoluteValue.Completion.algebraMap_eq

added theorem AbsoluteValue.Completion.algebraMap_eq_of_liesOver

deleted theorem AbsoluteValue.Completion.algebra_eq

added theorem AbsoluteValue.Completion.algebra_eq_of_liesOver

added theorem AbsoluteValue.Completion.coe_add

added theorem AbsoluteValue.Completion.coe_inv

added theorem AbsoluteValue.Completion.coe_mul

added theorem AbsoluteValue.Completion.coe_neg

added theorem AbsoluteValue.Completion.coe_one

added theorem AbsoluteValue.Completion.coe_sub

added theorem AbsoluteValue.Completion.coe_zero

added theorem AbsoluteValue.Completion.continuous_coe

added theorem AbsoluteValue.Completion.continuous_map

added theorem AbsoluteValue.Completion.continuous_ofCompletion

added theorem AbsoluteValue.Completion.continuous_toCompletion

added theorem AbsoluteValue.Completion.denseRange_coe

added def AbsoluteValue.Completion.equiv

added theorem AbsoluteValue.Completion.equiv_apply

added theorem AbsoluteValue.Completion.equiv_symm_apply

added theorem AbsoluteValue.Completion.ext

added theorem AbsoluteValue.Completion.induction_on

added theorem AbsoluteValue.Completion.isometry_map

added theorem AbsoluteValue.Completion.isometry_ofCompletion

added theorem AbsoluteValue.Completion.isometry_toCompletion

added theorem AbsoluteValue.Completion.map_coe

added theorem AbsoluteValue.Completion.norm_coe

added theorem AbsoluteValue.Completion.norm_ofCompletion

added theorem AbsoluteValue.Completion.norm_toCompletion

added theorem AbsoluteValue.Completion.ofCompletion_algebraMap

added theorem AbsoluteValue.Completion.ofCompletion_coe

added theorem AbsoluteValue.Completion.ofCompletion_inj

added theorem AbsoluteValue.Completion.ofCompletion_injective

added theorem AbsoluteValue.Completion.ofCompletion_surjective

added theorem AbsoluteValue.Completion.ofCompletion_toCompletion

added theorem AbsoluteValue.Completion.toCompletion_algebraMap

added theorem AbsoluteValue.Completion.toCompletion_coe

added theorem AbsoluteValue.Completion.toCompletion_inj

added theorem AbsoluteValue.Completion.toCompletion_injective

added theorem AbsoluteValue.Completion.toCompletion_ofCompletion

added theorem AbsoluteValue.Completion.toCompletion_surjective

added structure AbsoluteValue.Completion

Modified Mathlib/NumberTheory/NumberField/AdeleRing.lean

Modified Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean

modified theorem NumberField.InfinitePlace.Completion.algebraMap_apply

modified theorem NumberField.InfinitePlace.Completion.coe_add

modified theorem NumberField.InfinitePlace.Completion.coe_mul

Modified Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean

Modified Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

modified theorem NumberField.InfiniteAdeleRing.algebraMap_apply

modified theorem NumberField.InfiniteAdeleRing.denseRange_algebraMap