Krull–Akizuki in Lean 4/Mathlib via R-lengths: removes separability from Dedekind integral closure

Mathlib (v4.35-era) has IsIntegralClosure.isDedekindDomain only for separable L/K; Noetherianity is the only part that needs it. Krull–Akizuki fills the gap in ~500 lines using only Module.length over R. (1) l(N ⧸ Q) = l(P.map Q.mkQ) + l(N ⧸ P) from length_eq_add_of_exact with Submodule.factor. (2) l(N ⧸ a^t•⊤) ≤ t·l(N ⧸ a•⊤), with equality for regular a, via the map x ↦ [a^t x] into N ⧸ a^(t+1)•⊤ and quotKerEquivRange. (3) The span bound via Fintype.linearCombination + Submodule.quotientPi + length_pi_of_fintype. (4) Mathlib's isFiniteLength_quotient_span_singleton (Noetherian, KrullDimLE 1) gives the finiteness of R ⧸ (c). (5) Exhaustion: a module whose f.g. submodules have length ≤ C has length ≤ C; take a max-length f.g. S and use Submodule.length_lt. A nonzero ideal of S meets R via Ideal.under_ne_bot_of_algebraic_mem; isNoetherian_of_tower and isArtinian_of_tower move finiteness from R to S. Instance gotcha: R ⧸ (I : Ideal R) and R ⧸ (I : Submodule R R) carry different Module instances; mixing them caused heartbeat timeouts, so state length lemmas with Submodule R R.