Theorems · Theorem · linear algebra

Matrix.cRank_toNat_eq_finrank

∀ {m : Type um} {n : Type un} {R : Type uR} [inst : Semiring R] (A : Matrix m n R),
  Cardinal.toNat A.cRank = Module.finrank R ↥(Submodule.span R (Set.range A.col))

Defined in

Mathlib.LinearAlgebra.Matrix.Rank

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring