English
If A ⊗F B is a field, then A and B embed into a common field with linear disjointness of the images.
Русский
Если A ⊗F B — поле, тогда A и B внедряются в общее поле образами, линейно независимыми между собой.
LaTeX
$$$\text{If } A \otimes_F B \text{ is a field, then } A \text{ and } B \text{ are linearly disjoint over } F$$$
Lean4
/-- If `A ⊗[F] L` is a field, then `A` and `L` are linearly disjoint over `F`. -/
theorem of_isField (H : IsField (A ⊗[F] L)) : A.LinearDisjoint L :=
by
apply Subalgebra.LinearDisjoint.of_isField
haveI : SMulCommClass F A A := SMulCommClass.of_commMonoid F A A
haveI : SMulCommClass F A.toSubalgebra A.toSubalgebra := ‹SMulCommClass F A A›
letI : Mul (A ⊗[F] L) := Algebra.TensorProduct.instMul
letI : Mul (A.toSubalgebra ⊗[F] (IsScalarTower.toAlgHom F L E).range) := Algebra.TensorProduct.instMul
exact
Algebra.TensorProduct.congr (AlgEquiv.refl : A ≃ₐ[F] A)
(AlgEquiv.ofInjective (IsScalarTower.toAlgHom F L E) (RingHom.injective _)) |>.symm.toMulEquiv.isField
H
