theorem
integralClosure_isDVR
(A : Type u_1)
[CommRing A]
[IsDomain A]
[IsDiscreteValuationRing A]
[IsAdicComplete (IsLocalRing.maximalIdeal A) A]
(K : Type u_2)
[Field K]
[Algebra A K]
[IsFractionRing A K]
(E : Type u_3)
[Field E]
[Algebra K E]
[FiniteDimensional K E]
[Algebra.IsSeparable K E]
[Algebra A E]
[IsScalarTower A K E]
: