English
If there exist embeddings of A and B into a field K such that their images are linearly disjoint, then A ⊗F B is a domain and there exists a field extension realizing this.
Русский
Если существуют вложения A и B в поле K такие, что их образы линейно раздельны, то A ⊗F B является областью и можно реализовать это через некоторое расширение поля.
LaTeX
$$$\exists K, fa, fb \text{ с } fa.fieldRange.LinearDisjoint fb.fieldRange$$$
Lean4
/-- If `A` and `L` have coprime degree over `F`, then they are linearly disjoint. -/
theorem of_finrank_coprime (H : (finrank F A).Coprime (finrank F L)) : A.LinearDisjoint L :=
letI : Field (AlgHom.range (IsScalarTower.toAlgHom F L E)) :=
inferInstanceAs <| Field (AlgHom.fieldRange (IsScalarTower.toAlgHom F L E))
letI : Field A.toSubalgebra := inferInstanceAs <| Field A
Subalgebra.LinearDisjoint.of_finrank_coprime_of_free <| by
rwa [(AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F L E)).toLinearEquiv.finrank_eq] at H
