det_fromBlocks_one₂₂ — Mathlib

English

When the bottom-right block is 1, the determinant of fromBlocks(A,B,C,1) equals det(A − B C).

Русский

Если нижний правый блок равен единице, то det fromBlocks(A,B,C,1) = det(A − B C).

LaTeX

$$$\\det\\mathrm{fromBlocks}(A,B,C,1) = \\det\\bigl(A - B C\\bigr)$$$

Lean4

@[simp]
theorem det_fromBlocks_one₂₂ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α) :
    (Matrix.fromBlocks A B C 1).det = det (A - B * C) :=
  by
  haveI : Invertible (1 : Matrix n n α) := invertibleOne
  rw [det_fromBlocks₂₂, invOf_one, Matrix.mul_one, det_one, one_mul]

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