English
If L is a finite separable extension and A is a principal ideal ring with NoZeroSmulDivisors assumptions, then the A-rank of the integral closure C of A in L equals the K-rank of L.
Русский
Пусть L — конечное сепарабельноe расширение и A — кольцо с выводом ПР, удовлетворяющее условиям NoZeroSmulDivisors. Тогда A-ранг интегрального замыкания C в L равен K-рангу L.
LaTeX
$$$$\\operatorname{finrank}_A(C) = \\operatorname{finrank}_K(L)$$$$
Lean4
/-- If `L` is a finite separable extension of `K = Frac(A)`, where `A` is
integrally closed and Noetherian, the integral closure `C` of `A` in `L` is
finite over `A`. -/
theorem finite [IsIntegrallyClosed A] [IsNoetherianRing A] : Module.Finite A C :=
by
haveI := IsIntegralClosure.isNoetherian A K L C
exact Module.IsNoetherian.finite A C
