English
Let R be a commutative ring, and A,B be subalgebras of S over R which are linearly disjoint and free as R-modules. Then the finite rank of the join A ⊔ B equals the product of the finite ranks of A and B:
Русский
Пусть R — коммутативное кольцо, A и B — подалгебры S над R, пара линейно дизайнтов и свободны как R-модули. Тогда конечная размерность (ранг) объединения A ⊔ B равна произведению рангов A и B:
LaTeX
$$$\\displaystyle \\operatorname{finrank}_R(A \\vee B) = \\operatorname{finrank}_R(A) \\cdot \\operatorname{finrank}_R(B).$$$
Lean4
/-- In a commutative ring, if subalgebras `A` and `B` are linearly disjoint and they are
free modules, then the rank of `A ⊔ B` is equal to the product of the rank of `A` and `B`. -/
theorem finrank_sup_of_free [Module.Free R A] [Module.Free R B] :
Module.finrank R ↥(A ⊔ B) = Module.finrank R A * Module.finrank R B := by
simpa only [map_mul] using congr(Cardinal.toNat $(H.rank_sup_of_free))
