rank_matrix'' — Mathlib

English

For a finite index set η, the rank of the product of modules ∀ i, φ i equals the sum of ranks of φ i.

Русский

Пусть η конечен; ранг модуля типа функций ∀ i, φ i равен сумме рангов каждый φ i.

LaTeX

$$$\operatorname{rank}_R\bigl(\forall i, \phi(i)\bigr) = \displaystyle \sum_{i} \operatorname{rank}_R(\phi(i))$$$

Lean4

/-- If `m` and `n` are finite and lie in the same universe as `R`, the rank of `m × n` matrices
  is `# m * # n`. -/
theorem rank_matrix'' (m n : Type u) [Finite m] [Finite n] : Module.rank R (Matrix m n R) = #m * #n := by simp

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