English
If m, n are finite, then rank_R(Matrix m×n M) = lift(lift(rank_R M)) times a product: rank = lift(#m) * lift(#n) * lift(rank_R M).
Русский
Пусть m, n конечны. Тогда ранг Matrix m×n M равен lift(#m) · lift(#n) · lift(rank_R M).
LaTeX
$$$\operatorname{rank}_R(\mathrm{Matrix}_{m,n} M) = \operatorname{lift}(\#m) \cdot \operatorname{lift}(\#n) \cdot \operatorname{lift}(\operatorname{rank}_R M)$$$
Lean4
/-- If `m` and `n` are finite, the rank of `m × n` matrices over a module `M` is
`(#m).lift * (#n).lift * rank R M`. -/
@[simp]
theorem rank_matrix_module (m : Type w) (n : Type w') [Finite m] [Finite n] :
Module.rank R (Matrix m n M) = lift.{max v w'} #m * lift.{max v w} #n * lift.{max w w'} (Module.rank R M) :=
by
cases nonempty_fintype m
cases nonempty_fintype n
obtain ⟨I, b⟩ := Module.Free.exists_basis (R := R) (M := M)
rw [← (b.matrix m n).mk_eq_rank'']
simp only [mk_prod, lift_mul, lift_lift, ← mul_assoc, b.mk_eq_rank'']
