English
If A and B are field extensions of F and there exist embeddings A → E and B → E into some field E with linearly disjoint images, then A ⊗F B is a field.
Русский
Если A и B — поля, расширяющие F, и существуют вложения A → E и B → E в некоторый поле E, чьи образы линейно независимы, то A ⊗F B является полем.
LaTeX
$$$\\text{If } A,B \\text{ are }F\\text{-fields and there exist injective }F\\text{-algebras }A \\to E, B \\to E\\text{ with } A\\text{-image } \\text{LinearDisjoint } B\\text{-image, then } A \\otimes_F B \\text{ is a field.}$$$
Lean4
/-- If `A` and `B` are field extensions of `F`, one of them is algebraic, such that there exists a
field `E` that `A` and `B` embeds into with linearly disjoint images, then `A ⊗[F] B`
is a field. -/
theorem isField_of_isAlgebraic' {A B : Type*} [Field A] [Algebra F A] [Field B] [Algebra F B] {fa : A →ₐ[F] E}
{fb : B →ₐ[F] E} (H : fa.fieldRange.LinearDisjoint fb.fieldRange)
(halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F B) : IsField (A ⊗[F] B) :=
have := H.isDomain'
Algebra.TensorProduct.isField_of_isAlgebraic F A B halg
