English
Suppose A and B are finite-dimensional over F and the dimension of their join equals the product of their dimensions. Then A and B are linearly disjoint over F.
Русский
Пусть A и B имеют конечную размерность над F, и измерение A ⊔ B равно произведению размерностей A и B. Тогда A и B линейно независимы над F.
LaTeX
$$$[\operatorname{finrank}_F A] \perp [\operatorname{finrank}_F B] \,\Rightarrow\, A \text{ линейно независимы над } F$$$
Lean4
/-- If `A` and `B` are finite extensions of `F`,
such that rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`,
then `A` and `B` are linearly disjoint. -/
theorem of_finrank_sup [FiniteDimensional F A] [FiniteDimensional F B]
(H : finrank F ↥(A ⊔ B) = finrank F A * finrank F B) : A.LinearDisjoint B :=
linearDisjoint_iff'.2 <| .of_finrank_sup_of_free (by rwa [← sup_toSubalgebra_of_left])
