Theorems · Theorem · commutative algebra

IsStronglyTranscendental.of_transcendental

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {K : Type u_4}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : Algebra S K] [IsScalarTower R S K] [FaithfulSMul R S]
  [FaithfulSMul S K] {x : S}, Transcendental R ((algebraMap S K) x) → IsStronglyTranscendental R x

Defined in

Mathlib.RingTheory.Algebraic.StronglyTranscendental

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFieldAlgebraAlgebraIsScalarTowerFaithfulSMulFaithfulSMul