Theorems · Theorem · field theory

algebraicIndependent_of_set_of_finite

∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A] (s : Set ι),
  (AlgebraicIndependent R fun i => x ↑i) →
    (∀ (t : Set ι),
        t.Finite →
          (AlgebraicIndependent R fun i => x ↑i) →
            ∀ i ∉ s, i ∉ t → Transcendental (↥(Algebra.adjoin R (x '' t))) (x i)) →
      AlgebraicIndependent R x

Defined in

Mathlib.RingTheory.AlgebraicIndependent.Transcendental

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra