English
Let R,S be commutative rings, A,B subalgebras of S with A,B as above and with free structures as in the hypotheses. Then the rank of the join A ⊔ B over R equals the product of ranks: rank_R(A ⊔ B) = rank_R(B) · rank_B(Algebra.adjoin(B, A:Set S)).
Русский
Пусть R,S — коммутативные кольца, A,B — подполья S, удовлетворяющие условиям свободы. Тогда ранг объединения A ⊔ B над R равен произведению рангов: rank_R(A ⊔ B) = rank_R(B) · rank_B(Algebra.adjoin(B, A)).
LaTeX
$$$\operatorname{rank}_R \; \big(\mathrm{A} \sqcup \mathrm{B}\big) = \operatorname{rank}_R \mathrm{B} \cdot \operatorname{rank}_{\mathrm{B}} \big(\operatorname{Algebra.adjoin} \mathrm{B} (\mathrm{A} : \mathrm{Set} S)\big)$$$
Lean4
theorem rank_sup_eq_rank_right_mul_rank_of_free :
Module.rank R ↥(A ⊔ B) = Module.rank R B * Module.rank B (Algebra.adjoin B (A : Set S)) := by
rw [sup_comm, rank_sup_eq_rank_left_mul_rank_of_free]
