Theorems · Theorem · linear algebra

rank_matrix

∀ (R : Type u) [inst : Semiring R] [StrongRankCondition R] (m : Type v) (n : Type w) [Finite m] [Finite n],
  Module.rank R (Matrix m n R) =
    Cardinal.lift.{max v w u, v} (Cardinal.mk m) * Cardinal.lift.{max v w u, w} (Cardinal.mk n)

If m and n are finite, the rank of m × n matrices is (#m).lift * (#n).lift.

Defined in

Mathlib.LinearAlgebra.Dimension.Constructions

Cited by

1 results in Mathlib

Foundations

Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringStrongRankConditionFiniteFinite