English
There exists a field K into which A and B embed with linear disjointness when A ⊗F B is a domain.
Русский
Существует поле K, куда A и B вводятся линейно независимыми, если A ⊗F B — область.
LaTeX
$$$\exists K fa fb \; (fa.fieldRange.LinearDisjoint fb.fieldRange)$$$
Lean4
/-- If `A` and `B` are field extensions of `F`, such that `A ⊗[F] B` is a domain, then there exists
a field extension of `F` that `A` and `B` embed into with linearly disjoint images. -/
theorem exists_field_of_isDomain (A : Type v) [Field A] (B : Type w) [Field B] [Algebra F A] [Algebra F B]
[IsDomain (A ⊗[F] B)] :
∃ (K : Type (max v w)) (_ : Field K) (_ : Algebra F K) (fa : A →ₐ[F] K) (fb : B →ₐ[F] K),
fa.fieldRange.LinearDisjoint fb.fieldRange :=
have ⟨K, inst1, inst2, fa, fb, _, _, H⟩ :=
Subalgebra.LinearDisjoint.exists_field_of_isDomain_of_injective F A B (RingHom.injective _) (RingHom.injective _)
⟨K, inst1, inst2, fa, fb, linearDisjoint_iff'.2 H⟩
