Theorems · Theorem · commutative algebra

isAlgebraic_of_isFractionRing

∀ (R : Type u_5) (S : Type u_6) (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Field K] [inst_3 : CommRing L] [inst_4 : Algebra R S] [inst_5 : Algebra R K] [inst_6 : Algebra R L]
  [inst_7 : Algebra S L] [inst_8 : Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] [IsFractionRing S L]
  [Algebra.IsIntegral R S], Algebra.IsAlgebraic K L

Defined in

Mathlib.RingTheory.Localization.Integral

Cited by

6 results in Mathlib

Foundations

Depth 134 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingFieldCommRingAlgebraAlgebraAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerIsFractionRingAlgebra.IsIntegral