English
If A and B are linearly disjoint and free as R-modules, then rank(A ⊔ B) = rank(A) * rank(B).
Русский
Если A и B линейно раздельны и свободны как модули над R, то ранг объединения равен произведению рангов.
LaTeX
$$$A \\perp_L B \\land \\text{Module.Free}_R(A) \\land \\text{Module.Free}_R(B) \\Rightarrow \\operatorname{rank}_R(A\\amalg B) = \\operatorname{rank}_R(A) \\cdot \\operatorname{rank}_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 rank_sup_of_free [Module.Free R A] [Module.Free R B] :
Module.rank R ↥(A ⊔ B) = Module.rank R A * Module.rank R B :=
by
nontriviality R
rw [← rank_tensorProduct', H.mulMap.toLinearEquiv.rank_eq]
