Polynomial growth of ideal counts at prime powers

An ideal of norm p^k is determined by the multiplicities of the prime ideals above p. Each multiplicity is at most k, and there are at most [K:ℚ] such prime ideals.

theorem NairTenenbaum.rationalPrimeBelow_eq_of_dvd_primePowerNorm {K : Type u_1} [Field K] [NumberField K] {P I : Ideal (NumberField.RingOfIntegers K)} (hP : Prime P) {p k : ℕ} (hp : Nat.Prime p) (hI : Ideal.absNorm I = p ^ k) (hd : P ∣ I) : rationalPrimeBelow P = p

theorem NairTenenbaum.ideal_factor_count_le_primePowerNorm {K : Type u_1} [Field K] [NumberField K] {I P : Ideal (NumberField.RingOfIntegers K)} {p k : ℕ} (hp : Nat.Prime p) (hI : Ideal.absNorm I = p ^ k) : Multiset.count P (UniqueFactorizationMonoid.normalizedFactors I) ≤ k

theorem NairTenenbaum.idealNormCount_prime_pow_le {K : Type u_1} [Field K] [NumberField K] {p k : ℕ} (hp : Nat.Prime p) : idealNormCount K (p ^ k) ≤ (k + 1) ^ Module.finrank ℚ K