finrank_tensorProduct — Mathlib

English

The rank of R ⊗_S M' over R equals the rank of M' over S, lifted to the appropriate universe.

Русский

Ранг пространства R ⊗_S M' над R равен рангу пространства M' над S, с переносом кардинала.

LaTeX

$$$ \\operatorname{Module.rank} R (R \\otimes_S M') = \\operatorname{Cardinal.lift} (\\operatorname{Module.rank} S M'). $$$

Lean4

/-- The `S`-`finrank` of `M ⊗[R] M'` is `(finrank S M) * (finrank R M')`. -/
@[simp]
theorem finrank_tensorProduct : finrank R (M ⊗[S] M') = finrank R M * finrank S M' := by simp [finrank]

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