English
If A and B are linearly disjoint over F, then the rank (dimension as F-vector space) of A ⊔ B equals the product rank(A) · rank(B).
Русский
Если A и B линейно разобщены над F, то размерности A ⊔ B над F равна произведению размерностей A и B над F.
LaTeX
$$$\operatorname{rank}_F(A \vee B) = \operatorname{rank}_F A \cdot \operatorname{rank}_F B$$$
Lean4
/-- If `A` and `B` are linearly disjoint over `F`, then the
rank of `A ⊔ B` is equal to the product of that of `A` and `B`. -/
theorem rank_sup (H : A.LinearDisjoint B) : Module.rank F ↥(A ⊔ B) = Module.rank F A * Module.rank F B :=
have h := le_sup_toSubalgebra A B
(rank_sup_le A B).antisymm <|
(linearDisjoint_iff'.1 H).rank_sup_of_free.ge.trans <|
(Subalgebra.inclusion h).toLinearMap.rank_le_of_injective (Subalgebra.inclusion_injective h)
