rank_matrix_module' — Mathlib

English

For finite m, n, rank of Matrix m n M equals lift(#m * #n) times lift(rank_R M).

Русский

Для конечных m, n ранг Matrix m n M равен lift(#m · #n) умноженному на lift(rank_R M).

LaTeX

$$$\operatorname{rank}_R(\mathrm{Matrix}_{m,n} M) = \operatorname{lift}(\#m \cdot \#n) \cdot \operatorname{lift}(\operatorname{rank}_R M)$$$

Lean4

/-- If `m` and `n` are finite and lie in the same universe, the rank of `m × n` matrices over a
module `M` is `(#m * #n).lift * rank R M`. -/
@[simp high]
theorem rank_matrix_module' (m n : Type w) [Finite m] [Finite n] :
    Module.rank R (Matrix m n M) = lift.{max v} (#m * #n) * lift.{w} (Module.rank R M) := by
  rw [rank_matrix_module, lift_mul, lift_umax.{w, v}]

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