Commit 2025-05-07 16:46 20407390

View on Github →

feat(NumberField/Ideal): asymptotics for the number of integral ideals of bounded norm (#22866) Prove asymptotics for the number of integral ideals of bounded norm. This PR is part of the proof of the Analytic Class Number Formula.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean

added theorem nonZeroDivisors_dvd_iff_dvd_coe

Modified Mathlib/Algebra/Module/ZLattice/Covolume.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

added theorem measurableSet_frontier

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Created Mathlib/NumberTheory/NumberField/Ideal.lean

added theorem NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop

added theorem NumberField.Ideal.tendsto_norm_le_div_atTop

added theorem NumberField.Ideal.tendsto_norm_le_div_atTop₀

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

added theorem Ideal.finite_setOf_absNorm_le₀