English
If L is a finite extension of the fraction field of A, the integral closure C of A in L has fraction field L.
Русский
Если L является конечным расширением дробей поля дробей A, интегральное замыкание C A в L имеет поле дробей L.
LaTeX
$$$\operatorname{Frac}(\mathrm{integralClosure}(A,L)) \cong L$$$
Lean4
/-- If the field `L` is a finite extension of the fraction field of the integral domain `A`,
the integral closure `C` of `A` in `L` has fraction field `L`. -/
theorem isFractionRing_of_finite_extension [IsDomain A] [Algebra K L] [IsScalarTower A K L] [FiniteDimensional K L] :
IsFractionRing C L :=
have : Algebra.IsAlgebraic A L := IsFractionRing.comap_isAlgebraic_iff.mpr (inferInstanceAs (Algebra.IsAlgebraic K L))
isFractionRing_of_algebraic A C fun _ hx =>
IsFractionRing.to_map_eq_zero_iff.mp
((map_eq_zero <| algebraMap K L).mp <| (IsScalarTower.algebraMap_apply _ _ _ _).symm.trans hx)
