The integral closure of a Dedekind domain in a finite separable extension is finite

[kbuzzard]

Is it true that if A is a Dedekind domain with field of fractions K, and if L/K is a finite separable extension, then the integral closure B of A in L is a finite A-module? I'm assuming so but was reluctant to add it as an assumption if it was not true in this generality. This is

example : Module.Finite A B := by sorry -- I assume this is correct

in FLT.DedekindDomain.FiniteAdeleRing.BaseChange .

[4hma4d]

It seems to be true by this

[4hma4d]

claim

[alreadydone]

I also found a reference to Milne, and a reference to a counterexample in the inseparable case. (Krull--Akizuki implies the integral closure is a Dedekind domain even in the inseparable case.)
This paper is also tangentially relevant (a Japanese domain is one whose integral closure in any finite extension of its field of fractions is finite).

[4hma4d]

propose #211

[Ruben-VandeVelde]

This is done in 2473f61

[kbuzzard]

Thanks!