Theorems · Theorem · commutative algebra

Algebra.IsPushout.isAlgebraic

∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [alg : Algebra.IsAlgebraic R S] (R' : Type u_4) [inst_3 : CommRing R'] [inst_4 : Algebra R R'] [NoZeroDivisors R']
  [FaithfulSMul R R'] (S' : Type u_5) [inst_7 : CommRing S'] [inst_8 : Algebra R S'] [inst_9 : Algebra S S']
  [inst_10 : Algebra R' S'] [inst_11 : IsScalarTower R R' S'] [inst_12 : IsScalarTower R S S']
  [h : Algebra.IsPushout R S R' S'], Algebra.IsAlgebraic R' S'

Defined in

Mathlib.RingTheory.Algebraic.Integral

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraAlgebra.IsAlgebraicCommRingAlgebraNoZeroDivisorsFaithfulSMulCommRingAlgebraAlgebraAlgebraIsScalarTowerIsScalarTowerAlgebra.IsPushout