English
If A and L are linearly disjoint over F and one of them is algebraic over F, then for any B and L' isomorphic to A and L respectively, B and L' are also linearly disjoint, hence A ⊗F L is a field.
Русский
Если A и L линейно независимы над F и одно из них алгебраическое над F, то при любой B и L', изоморфных A и L соответственно, B и L' тоже линейно независимы; следовательно A ⊗F L является полем.
LaTeX
$$$(A \\text{ LinearDisjoint } L) \\land (\\text{Algebra.IsAlgebraic } F A \\lor \\text{Algebra.IsAlgebraic } F L) \\Rightarrow IsField(A \\otimes_{F} L)$$$
Lean4
/-- If `A` and `L` are linearly disjoint over `F` and one of them is algebraic,
then `A ⊗[F] L` is a field. -/
theorem isField_of_isAlgebraic (H : A.LinearDisjoint L) (halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F L) :
IsField (A ⊗[F] L) :=
have := H.isDomain
Algebra.TensorProduct.isField_of_isAlgebraic F A L halg
