English
The rank of a tensor product M ⊗_S M' over R equals the product of the lifts of the ranks of M and M'.
Русский
Ранг тензорного произведения M ⊗_S M' над R равен произведению их рангов, с учётом переносов кардиналов: rank_R(M ⊗_S M') = lift(rank_R M) · lift(rank_S M').
LaTeX
$$$ \\operatorname{Module.rank} R (M \\otimes_S M') = \\operatorname{Cardinal.lift} (\\operatorname{Module.rank} R M) \\cdot \\operatorname{Cardinal.lift} (\\operatorname{Module.rank} S M'). $$$
Lean4
/-- The `S`-rank of `M ⊗[R] M'` is `(Module.rank S M).lift * (Module.rank R M').lift`. -/
@[simp]
theorem rank_tensorProduct :
Module.rank R (M ⊗[S] M') = Cardinal.lift.{v'} (Module.rank R M) * Cardinal.lift.{v} (Module.rank S M') :=
by
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)
obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')
rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]
