rank_prod' — Mathlib

English

If M and M' are free, then rank_R(M × M') = rank_R M + rank_R M'.

Русский

Если M и M' свободны, то ранг M × M' равен сумме рангов M и M'.

LaTeX

$$$\operatorname{rank}_R (M \times M') = \operatorname{rank}_R M + \operatorname{rank}_R M'$$$

Lean4

/-- If `M` and `M'` are free (and lie in the same universe), the rank of `M × M'` is
  `(Module.rank R M) + (Module.rank R M')`. -/
theorem rank_prod' : Module.rank R (M × M₁) = Module.rank R M + Module.rank R M₁ := by simp

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