English
If A,B are flat R-algebras and transcendental over R, then A ⊗_R B is not a field.
Русский
Если A,B плоские над R и трансцендентны над R, то A ⊗_R B не является полем.
LaTeX
$$$\\text{Algebra.Transcendental}_R(A) \\land \\text{Algebra.Transcendental}_R(B) \\Rightarrow \\lnot \\text{IsField}(A\\otimes_R B)$$$
Lean4
/-- If `A` and `B` are flat `R`-algebras, such that `A ⊗[R] B` is a field, then one of `A` and `B`
is algebraic over `R`. -/
theorem _root_.Algebra.TensorProduct.isAlgebraic_of_isField (A : Type v) [CommRing A] (B : Type w) [CommRing B]
[Algebra R A] [Algebra R B] [Module.Flat R A] [Module.Flat R B] (H : IsField (A ⊗[R] B)) :
Algebra.IsAlgebraic R A ∨ Algebra.IsAlgebraic R B :=
by
by_contra! h
simp_rw [← Algebra.transcendental_iff_not_isAlgebraic] at h
obtain ⟨_, _⟩ := h
exact Algebra.TensorProduct.not_isField_of_transcendental R A B H
