Commit 2026-05-23 07:31 9dd2956d

View on Github →

feat(NumberTheory/NumberField/Completion/FinitePlace): add multiplicity lemmas (#39008) This adds some more API for multiplicities of prime ideals in factorizations (and some more basic API lemmas, too), in preparation for a proof of the Northcott property for heights on number fields. We also extend the API for HasFinite{Mul|}Support a bit.

Estimated changes

Modified Mathlib/Algebra/FiniteSupport/Basic.lean

added theorem Function.HasFiniteSupport.hasFiniteMulSupport_fun_pow

added theorem Function.HasFiniteSupport.mul_left

added theorem Function.HasFiniteSupport.mul_right

added theorem Function.HasFiniteSupport.smul_left

added theorem Function.HasFiniteSupport.smul_right

added theorem Multiset.hasFiniteSupport_count

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

added theorem NumberField.FinitePlace.apply_mul_absNorm_pow_eq_one

added theorem NumberField.FinitePlace.finprod_finitePlace_pow_multiplicity

added theorem NumberField.FinitePlace.hasFiniteMulSupport_fun_pow_multiplicity

Modified Mathlib/RingTheory/Algebraic/Integral.lean

added theorem IsAlgebraic.exists_nsmul_eq

added theorem IsAlgebraic.exists_smul_eq

Modified Mathlib/RingTheory/DedekindDomain/Ideal/Lemmas.lean

added theorem IsDedekindDomain.HeightOneSpectrum.asIdeal_injective

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

added theorem UniqueFactorizationMonoid.hasFiniteMulSupport_fun_pow_multiplicity