det_fromBlocks_one₁₁ — Mathlib

English

When the top-left block is 1 (identity), the determinant of the block matrix fromBlocks(1,B,C,D) equals det(D − C B).

Русский

Если верхний левый блок равен единице, то детерминант fromBlocks(1,B,C,D) равен det(D − C B).

LaTeX

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

Lean4

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

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