Theorems · Theorem · field theory

IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_sdiff

∀ {ι : Type u} {R : Type u_1} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [FaithfulSMul R S] [NoZeroDivisors S] (s : Set ι) (i j : ι) (v : ι → S),
  j ∈ insert i s →
    (IsTranscendenceBasis R fun x => v ↑x) →
      IsAlgebraic (↥(Algebra.adjoin R (v '' (insert i s \ {j})))) (v j) → IsTranscendenceBasis R fun x => v ↑x

If s is a transcendence basis and j is algebraic over s ∪ {i} \ {j}, then s ∪ {i} \ {j} is also a transcendence basis.

Defined in

Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFaithfulSMulNoZeroDivisors