cramer_reindex — Mathlib

English

For an index isomorphism e, cramer(reindex e e A) b = cramer A (b ∘ e) ∘ e^{-1}.

Русский

Для отображения перестановки e справедливо: cramer(reindex e e A) b = cramer A (b ∘ e) ∘ e^{-1}.

LaTeX

$$$$\\mathrm{cramer}(\\mathrm{reindex}\n e e A)\\ b = \\mathrm{cramer}(A, (b \\circ e)) \\circ e^{-1}.$$$$

Lean4

theorem cramer_reindex (e : m ≃ n) (A : Matrix m m α) (b : n → α) :
    cramer (reindex e e A) b = cramer A (b ∘ e) ∘ e.symm :=
  cramer_submatrix_equiv _ _ _

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