Theorems · Definition · linear algebra

Matrix.eRank

{m : Type um} → {n : Type un} → {R : Type uR} → [Semiring R] → Matrix m n R → ℕ∞

The rank of a matrix, defined as the dimension of its column space, as a term in ℕ∞.

Defined in

Mathlib.LinearAlgebra.Matrix.Rank

Cited by

11 results in Mathlib

Foundations

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

Assumes

Semiring