Theorems · Theorem · field theory

IsTranscendenceBasis.sumElim_comp

∀ {ι : Type u} {ι' : Type u'} {R : Type u_1} {S : Type v} {A : Type w} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : CommRing A] [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A]
  [NoZeroDivisors A] {x : ι → S} {y : ι' → A},
  IsTranscendenceBasis R x → IsTranscendenceBasis S y → IsTranscendenceBasis R (Sum.elim y (⇑(algebraMap S A) ∘ x))

Defined in

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraAlgebraIsScalarTowerNoZeroDivisors