rank_tensorProduct' — Mathlib

English

Under universes alignment, the same rank formula for tensor products holds with lifted cardinals.

Русский

При согласовании вселенных та же формула ранга для тензорного произведения сохраняется с переносами кардиналов.

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

/-- If `M` and `M'` lie in the same universe, the `S`-rank of `M ⊗[R] M'` is
  `(Module.rank S M) * (Module.rank R M')`. -/
theorem rank_tensorProduct' : Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁ := by simp

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