English
If A and B are linearly disjoint over F, and there are isomorphisms relating A to other subfields and B to another, the corresponding tensor product is a field.
Русский
Если A и B линейно несвязаны над F и существуют изоморфизмы между ними и другими подполями, соответствующее тензорное произведение является полем.
LaTeX
$$$A \\text{ LinearDisjoint } B \\Rightarrow IsField(A \\otimes_{F} B) \\text{ under suitable identifications.}$$$
Lean4
/-- If `A` and `L` are linearly disjoint, one of them is algebraic, then for any `B` and `L'`
isomorphic to `A` and `L` respectively, `B` and `L'` are also linearly disjoint. -/
theorem algEquiv_of_isAlgebraic (H : A.LinearDisjoint L) {E' : Type*} [Field E'] [Algebra F E']
(B : IntermediateField F E') (L' : Type*) [Field L'] [Algebra F L'] [Algebra L' E'] [IsScalarTower F L' E']
(f1 : A ≃ₐ[F] B) (f2 : L ≃ₐ[F] L') (halg : Algebra.IsAlgebraic F A ∨ Algebra.IsAlgebraic F L) :
B.LinearDisjoint L' :=
.of_isField ((Algebra.TensorProduct.congr f1 f2).symm.toMulEquiv.isField (H.isField_of_isAlgebraic halg))
