lift_cRank_reindex — Mathlib

English

Left/right reindexing preserves the lifted cRank: lift(cRank(A.reindex em en)) = lift(cRank(A)).

Русский

Переиндексация слева/справа сохраняет вознесённый cRank: lift(cRank(A.reindex em en)) = lift(cRank(A)).

LaTeX

$$$\operatorname{lift}(cRank(A^{\text{reindex }(em,en)})) = \operatorname{lift}(cRank(A))$$$

Lean4

theorem lift_cRank_reindex {n : Type un} (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) :
    lift.{um} (cRank (A.reindex em en)) = lift.{um₀} (cRank A) :=
  lift_cRank_submatrix ..

Похожие утверждения