adjugate_submatrix_equiv_self — Mathlib

English

If e: n ≃ m is an equivalence, then adjugate(A.submatrix e e) = (adjugate A).submatrix e e.

Русский

При эквивариантности e: n ≃ m выполняется adjugate(A.submatrix e e) = (adjugate A).submatrix e e.

LaTeX

$$$$\\operatorname{adjugate}(A_{submatrix\\ e\\ e}) = (\\operatorname{adjugate} A)_{submatrix\\ e\\ e}.$$$$

Lean4

@[simp]
theorem adjugate_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m α) :
    adjugate (A.submatrix e e) = (adjugate A).submatrix e e :=
  by
  ext i j
  have : (fun j ↦ Pi.single i 1 <| e.symm j) = Pi.single (e i) 1 := Function.update_comp_equiv (0 : n → α) e.symm i 1
  rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e, updateRow_submatrix_equiv, this]

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