Commit 2026-03-14 13:47 55aa437f

View on Github →

chore(NumberTheory/NumberField): move number field completion material to new subdir (#36393)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/NumberField/Completion/FinitePlace.lean

added theorem IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

added theorem IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply

added theorem NumberField.FinitePlace.add_le

added theorem NumberField.FinitePlace.coe_apply

added theorem NumberField.FinitePlace.embedding_apply

added theorem NumberField.FinitePlace.hasFiniteMulSupport

added theorem NumberField.FinitePlace.hasFiniteMulSupport_int

added theorem NumberField.FinitePlace.isFinitePlace

added theorem NumberField.FinitePlace.maximalIdeal_inj

added theorem NumberField.FinitePlace.maximalIdeal_injective

added theorem NumberField.FinitePlace.maximalIdeal_mk

added theorem NumberField.FinitePlace.mk_apply

added theorem NumberField.FinitePlace.mk_eq_iff

added theorem NumberField.FinitePlace.mk_maximalIdeal

added theorem NumberField.FinitePlace.norm_def

added theorem NumberField.FinitePlace.norm_embedding'

added theorem NumberField.FinitePlace.norm_embedding

added theorem NumberField.FinitePlace.norm_embedding_eq

added theorem NumberField.FinitePlace.norm_embedding_int

added theorem NumberField.FinitePlace.norm_eq_one_iff_notMem

added theorem NumberField.FinitePlace.norm_le_one

added theorem NumberField.FinitePlace.norm_lt_one_iff_mem

added theorem NumberField.FinitePlace.pos_iff

added def NumberField.FinitePlace

added def NumberField.IsFinitePlace

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal

added theorem NumberField.isFinitePlace_iff

added theorem NumberField.rankOne_hom'_def

added theorem NumberField.toNNReal_valued_eq_adicAbv

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

added theorem NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion

added theorem NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv

added theorem NumberField.InfinitePlace.Completion.algebraMap_coe

added theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbeddingOfIsReal

added theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isComplex

added def NumberField.InfinitePlace.Completion.extensionEmbedding

added def NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal

added theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply

added theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe

added theorem NumberField.InfinitePlace.Completion.extensionEmbedding_coe

added theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingOfIsReal

added def NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex

added def NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal

added theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal

added theorem NumberField.InfinitePlace.Completion.liesOver_conjugate_extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding

added theorem NumberField.InfinitePlace.Completion.norm_coe

added def NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex

added def NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal

added theorem NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex

added theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbeddingOfIsReal

added theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex

added theorem NumberField.InfinitePlace.LiesOver.embedding_liesOver_of_isReal

added theorem NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal

added theorem NumberField.InfinitePlace.LiesOver.isometry_algebraMap

added theorem NumberField.InfinitePlace.isometry_embedding

added theorem NumberField.InfinitePlace.isometry_embedding_of_isReal

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

deleted theorem IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply

deleted theorem NumberField.FinitePlace.add_le

deleted theorem NumberField.FinitePlace.coe_apply

deleted theorem NumberField.FinitePlace.embedding_apply

deleted theorem NumberField.FinitePlace.hasFiniteMulSupport

deleted theorem NumberField.FinitePlace.hasFiniteMulSupport_int

deleted theorem NumberField.FinitePlace.isFinitePlace

deleted theorem NumberField.FinitePlace.maximalIdeal_inj

deleted theorem NumberField.FinitePlace.maximalIdeal_injective

deleted theorem NumberField.FinitePlace.maximalIdeal_mk

deleted theorem NumberField.FinitePlace.mk_apply

deleted theorem NumberField.FinitePlace.mk_eq_iff

deleted theorem NumberField.FinitePlace.mk_maximalIdeal

deleted theorem NumberField.FinitePlace.norm_def

deleted theorem NumberField.FinitePlace.norm_embedding'

deleted theorem NumberField.FinitePlace.norm_embedding

deleted theorem NumberField.FinitePlace.norm_embedding_eq

deleted theorem NumberField.FinitePlace.norm_embedding_int

deleted theorem NumberField.FinitePlace.norm_eq_one_iff_notMem

deleted theorem NumberField.FinitePlace.norm_le_one

deleted theorem NumberField.FinitePlace.norm_lt_one_iff_mem

deleted theorem NumberField.FinitePlace.pos_iff

deleted def NumberField.FinitePlace

deleted def NumberField.IsFinitePlace

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm

deleted theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal

deleted theorem NumberField.isFinitePlace_iff

deleted theorem NumberField.rankOne_hom'_def

deleted theorem NumberField.toNNReal_valued_eq_adicAbv

Modified Mathlib/NumberTheory/NumberField/InfiniteAdeleRing.lean

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

deleted theorem NumberField.InfinitePlace.Completion.Rat.norm_infinitePlace_completion

deleted theorem NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv

deleted theorem NumberField.InfinitePlace.Completion.algebraMap_coe

deleted theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbeddingOfIsReal

deleted theorem NumberField.InfinitePlace.Completion.bijective_extensionEmbedding_of_isComplex

deleted def NumberField.InfinitePlace.Completion.extensionEmbedding

deleted def NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal

deleted theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_apply

deleted theorem NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe

deleted theorem NumberField.InfinitePlace.Completion.extensionEmbedding_coe

deleted theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbedding

deleted theorem NumberField.InfinitePlace.Completion.isClosed_image_extensionEmbeddingOfIsReal

deleted def NumberField.InfinitePlace.Completion.isometryEquivComplexOfIsComplex

deleted def NumberField.InfinitePlace.Completion.isometryEquivRealOfIsReal

deleted theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbedding

deleted theorem NumberField.InfinitePlace.Completion.isometry_extensionEmbeddingOfIsReal

deleted theorem NumberField.InfinitePlace.Completion.liesOver_conjugate_extensionEmbedding

deleted theorem NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding

deleted theorem NumberField.InfinitePlace.Completion.norm_coe

deleted def NumberField.InfinitePlace.Completion.ringEquivComplexOfIsComplex

deleted def NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal

deleted theorem NumberField.InfinitePlace.Completion.subfield_ne_real_of_isComplex

deleted theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbeddingOfIsReal

deleted theorem NumberField.InfinitePlace.Completion.surjective_extensionEmbedding_of_isComplex

deleted theorem NumberField.InfinitePlace.LiesOver.embedding_liesOver_of_isReal

deleted theorem NumberField.InfinitePlace.LiesOver.extensionEmbedding_liesOver_of_isReal

deleted theorem NumberField.InfinitePlace.LiesOver.isometry_algebraMap

deleted theorem NumberField.InfinitePlace.isometry_embedding

deleted theorem NumberField.InfinitePlace.isometry_embedding_of_isReal

Modified Mathlib/NumberTheory/NumberField/ProductFormula.lean