Theorems · Theorem · linear algebra

Matrix.eRank_submatrix_le

∀ {m : Type um} {m₀ : Type um₀} {n : Type un} {n₀ : Type un₀} {R : Type uR} [inst : Semiring R] (A : Matrix m n R)
  (r : m₀ → m) (c : n₀ → n), (A.submatrix r c).eRank ≤ A.eRank

Defined in

Mathlib.LinearAlgebra.Matrix.Rank

Cited by

0 results in Mathlib

Foundations

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

Assumes

Semiring