isFractionRing_of_finite_extension

English

If L is a finite extension of the fraction field of A, the integral closure of A in L has fraction field L.

Русский

Если L является конечным расширением дробей поля дробей A, интегральное замыкание 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 of `A` in `L` has fraction field `L`. -/
theorem isFractionRing_of_finite_extension [IsDomain A] [Algebra A L] [Algebra K L] [IsScalarTower A K L]
    [FiniteDimensional K L] : IsFractionRing (integralClosure A L) L :=
  IsIntegralClosure.isFractionRing_of_finite_extension A K L (integralClosure A L)

Похожие утверждения