Theorems · Theorem · linear algebra

Matrix.eRank_submatrix

∀ {m : Type um} {m₀ : Type um₀} {n₀ : Type un₀} {R : Type uR} {n : Type un} [inst : Semiring R] (A : Matrix m n R)
  (em : m₀ ≃ m) (en : n₀ ≃ n), (A.submatrix ⇑em ⇑en).eRank = A.eRank

Defined in

Mathlib.LinearAlgebra.Matrix.Rank

Cited by

1 results in Mathlib

Foundations

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

Assumes

Semiring