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]