isFractionRing_of_algebraic — Mathlib

English

If L is algebraic over A, the fraction field of the integral closure C of A in L is L.

Русский

Если L алгебраическое над A, то дробей поля C интегрального замыкания A в L равняется L.

LaTeX

$$$\operatorname{Frac}(\mathrm{integralClosure}(A,L)) = L$$$

Lean4

/-- If the field `L` is an algebraic extension of the integral domain `A`,
the integral closure of `A` in `L` has fraction field `L`. -/
theorem isFractionRing_of_algebraic [Algebra A L] [Algebra.IsAlgebraic A L] (inj : ∀ x, algebraMap A L x = 0 → x = 0) :
    IsFractionRing (integralClosure A L) L :=
  IsIntegralClosure.isFractionRing_of_algebraic A (integralClosure A L) inj

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