Theorems · Theorem · linear algebra

Matrix.lift_cRank_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),
  Cardinal.lift.{um, max uR um₀} (A.submatrix ⇑em ⇑en).cRank = Cardinal.lift.{um₀, max uR um} A.cRank

Defined in

Mathlib.LinearAlgebra.Matrix.Rank

Cited by

3 results in Mathlib

Foundations

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

Assumes

Semiring