Theorems · Theorem · field theory

AlgebraicIndependent.sumElim_iff

∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] {ι' : Type u_4} {y : ι' → A},
  AlgebraicIndependent R (Sum.elim y x) ↔
    AlgebraicIndependent R x ∧ AlgebraicIndependent (↥(Algebra.adjoin R (Set.range x))) y

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra