English
Let A and B be intermediate fields of E containing F, linearly disjoint over F. Then the F-dimension of their join A ⊔ B equals the product of their individual F-dimensions: [A ⊔ B : F] = [A : F] · [B : F].
Русский
Пусть A и B — промежуточные поля E над F, линейно независимы над F. Тогда размерность A ⊔ B над F равна произведению размерностей A над F и B над F: [A ⊔ B : F] = [A : F] · [B : F].
LaTeX
$$$\operatorname{finrank}_F\big( A \oplus B \big) = \operatorname{finrank}_F(A) \cdot \operatorname{finrank}_F(B)$$$
Lean4
/-- If `A` and `B` are linearly disjoint over `F`, then the `Module.finrank` of
`A ⊔ B` is equal to the product of that of `A` and `B`. -/
theorem finrank_sup (H : A.LinearDisjoint B) : finrank F ↥(A ⊔ B) = finrank F A * finrank F B := by
simpa only [map_mul] using congr(Cardinal.toNat $(H.rank_sup))
