cramer_submatrix_equiv — Mathlib

English

For a matrix A, an equivalence e, and b, cramer(A.submatrix e e) b = cramer A (b ∘ e.symm) ∘ e.

Русский

Для матрицы A и отображения эквивариантности e справедливо: cramer(A.submatrix e e) b = cramer A (b ∘ e.symm) ∘ e.

LaTeX

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

Lean4

theorem cramer_submatrix_equiv (A : Matrix m m α) (e : n ≃ m) (b : n → α) :
    cramer (A.submatrix e e) b = cramer A (b ∘ e.symm) ∘ e :=
  by
  ext i
  simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv, det_submatrix_equiv_self e, Function.comp_def]

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