Residue-degree totals and prime-norm ideal counts

theorem NairTenenbaum.primeIdealSupport_weighted_degree_eq {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : ∑ P : ↥(primeIdealSupport K p), (↑P).inertiaDeg ℤ * Multiset.count (↑P) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {↑p})) = Module.finrank ℚ K

theorem NairTenenbaum.primeIdealSupport_sum_inertiaDeg_le {K : Type u_1} [Field K] [NumberField K] {p : ℕ} (hp : Nat.Prime p) : ∑ P : ↥(primeIdealSupport K p), (↑P).inertiaDeg ℤ ≤ Module.finrank ℚ K