Commit 2026-07-13 08:45 a3364fae

View on Github →

refactor(NumberTheory): make InfinitePlace.Completion a one-field structure (#41543) Makes FLT a lot faster. InfinitePlace analogue of #41526.

Estimated changes

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

added theorem NumberField.InfinitePlace.Completion.algebraMap_apply

added theorem NumberField.InfinitePlace.Completion.algebraMap_eq_coe

added theorem NumberField.InfinitePlace.Completion.algebraMap_toCompletion

added theorem NumberField.InfinitePlace.Completion.coe_add

added theorem NumberField.InfinitePlace.Completion.coe_mul

added theorem NumberField.InfinitePlace.Completion.coe_one

added theorem NumberField.InfinitePlace.Completion.coe_toCompletion

added theorem NumberField.InfinitePlace.Completion.coe_zero

added theorem NumberField.InfinitePlace.Completion.continuous_coe

added theorem NumberField.InfinitePlace.Completion.continuous_ofCompletion

added theorem NumberField.InfinitePlace.Completion.continuous_toCompletion

added theorem NumberField.InfinitePlace.Completion.denseRange_coe

added def NumberField.InfinitePlace.Completion.equiv

added def NumberField.InfinitePlace.Completion.equivCompletion

added theorem NumberField.InfinitePlace.Completion.ext

modified def NumberField.InfinitePlace.Completion.extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.induction_on

added def NumberField.InfinitePlace.Completion.isometryEquivCompletion

added theorem NumberField.InfinitePlace.Completion.isometry_toCompletion

added theorem NumberField.InfinitePlace.Completion.norm_ofCompletion

added theorem NumberField.InfinitePlace.Completion.norm_toCompletion

added theorem NumberField.InfinitePlace.Completion.ofCompletion_surjective

added theorem NumberField.InfinitePlace.Completion.ofCompletion_toCompletion

added theorem NumberField.InfinitePlace.Completion.toCompletion_add

added theorem NumberField.InfinitePlace.Completion.toCompletion_mul

added theorem NumberField.InfinitePlace.Completion.toCompletion_ofCompletion

added theorem NumberField.InfinitePlace.Completion.toCompletion_one

added theorem NumberField.InfinitePlace.Completion.toCompletion_surjective

added theorem NumberField.InfinitePlace.Completion.toCompletion_zero

added structure NumberField.InfinitePlace.Completion

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

added theorem NumberField.LiesOver.completionMap_coe

added theorem NumberField.LiesOver.continuous_completionMap

Modified Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean