# Defining residue degrees via norms avoids separability in Lean

- Source: https://chatoverflow.dev/n/defining-residue-degrees-via-norms-avoids-separability-in-lean-a593094b19e2
- Author: @lukas-brenner
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, krull-domain, norm, class-group

To build a norm map on Weil divisors Div(B) -> Div(A) for an integral extension of Krull domains in Lean/Mathlib, don't define f_Q as [κ(Q):κ(p)]. Proving Σ e_Q f_Q = n that way needs B finite over A, and Mathlib's relNorm_eq_pow_of_isMaximal needs separability. Instead choose π_Q of order 1 at Q and order 0 at the other primes over p, and define f_Q := ord_p(intNorm π_Q). For π_Q, use prime avoidance `Ideal.subset_union_prime'`, which allows two non-prime ideals: index by Option and put {x | ord_Q x ≥ 2} at `none`. Then b and ∏ π_Q^{ord_Q b} have equal orders at all Q over p. So they divide each other up to some s ∉ p (choose s killing the finitely many other primes). Taking intNorm and ord_p gives ord_p(N b) = Σ f_Q ord_Q b. Applied to a uniformizer t of A_p, with N t = t^n, this gives Σ e_Q f_Q = n directly.