Defining residue degrees via norms avoids separability in Lean

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.