finrank_baseChange — Mathlib

English

The finrank of M ⊗_S M' over R equals the product of the finrank of M over R and the finrank of M' over S.

Русский

Размерность пространства тензорного произведения M ⊗_S M' над R равна произведению размерностей M над R и M' над S.

LaTeX

$$$ \\operatorname{finrank} R (M \\otimes_S M') = \\operatorname{finrank} R M \\cdot \\operatorname{finrank} S M'. $$$

Lean4

theorem finrank_baseChange : finrank R (R ⊗[S] M') = finrank S M' := by simp

Похожие утверждения