Theorems · Theorem · commutative algebra

Algebra.TensorProduct.not_isField_of_transcendental

∀ (R : Type u) [inst : CommRing R] (A : Type v) [inst_1 : CommRing A] (B : Type w) [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [Module.Flat R A] [Module.Flat R B] [Algebra.Transcendental R A]
  [Algebra.Transcendental R B], ¬IsField (TensorProduct R A B)

If A and B are flat R-algebras, both of them are transcendental, then A ⊗[R] B cannot be a field.

Defined in

Mathlib.RingTheory.LinearDisjoint

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraModule.FlatModule.FlatAlgebra.TranscendentalAlgebra.Transcendental