Commit 2025-02-28 20:55 75362b39

View on Github →

chore: renaming and documentation for NumberField.FinitePlace (#22407)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/FinitePlaces.lean

deleted theorem IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

deleted theorem IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply

deleted theorem NumberField.FinitePlace.apply

deleted theorem NumberField.FinitePlace.maximalIdeal_inj

deleted theorem NumberField.FinitePlace.maximalIdeal_injective

deleted theorem NumberField.FinitePlace.maximalIdeal_mk

deleted theorem NumberField.FinitePlace.mk_eq_iff

deleted theorem NumberField.FinitePlace.mk_maximalIdeal

deleted theorem NumberField.FinitePlace.mulSupport_finite

deleted theorem NumberField.FinitePlace.mulSupport_finite_int

deleted theorem NumberField.FinitePlace.norm_def'

deleted theorem NumberField.FinitePlace.norm_def

deleted theorem NumberField.FinitePlace.norm_def_int

deleted theorem NumberField.FinitePlace.norm_embedding_eq

deleted theorem NumberField.FinitePlace.pos_iff

deleted def NumberField.FinitePlace

added def NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.embedding

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.maximalIdeal_inj

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.maximalIdeal_injective

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.maximalIdeal_mk

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mk_apply

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mk_eq_iff

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mk_maximalIdeal

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mulSupport_finite

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.mulSupport_finite_int

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def'

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_def_int

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_embedding_eq

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_eq_one_iff_not_mem

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_le_one

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.norm_lt_one_iff_mem

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace.pos_iff

added def NumberField.RingOfIntegers.HeightOneSpectrum.FinitePlace

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.IsDedekindDomain.HeightOneSpectrum.equivHeightOneSpectrum_symm_apply

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal

added theorem NumberField.RingOfIntegers.HeightOneSpectrum.toNNReal_Valued_eq_vadicAbv

deleted def NumberField.embedding

deleted theorem NumberField.norm_eq_one_iff_not_mem

deleted theorem NumberField.norm_le_one

deleted theorem NumberField.norm_lt_one_iff_mem

deleted theorem NumberField.norm_ne_zero

deleted theorem NumberField.one_lt_norm

deleted theorem NumberField.one_lt_norm_nnreal

deleted theorem NumberField.toNNReal_Valued_eq_vadicAbv

deleted theorem NumberField.vadicAbv_add_le_max

deleted theorem NumberField.vadicAbv_def

deleted theorem NumberField.vadicAbv_intCast_le_one

deleted theorem NumberField.vadicAbv_natCast_le_one