English
The determinant of a matrix formed by fromBlocks with the upper-right block zero equals the product det(A) det(D).
Русский
Детерминант fromBlocks с нулевым верхним правым блоком равен произведению det(A) det(D).
LaTeX
$$$\\det(\\mathrm{fromBlocks} A 0 C D) = \\det A \\cdot \\det D$$$
Lean4
/-- The determinant of a 2×2 block matrix with the upper-right block equal to zero is the product of
the determinants of the diagonal blocks. For the generalization to any number of blocks, see
`Matrix.det_of_lowerTriangular`. -/
@[simp]
theorem det_fromBlocks_zero₁₂ (A : Matrix m m R) (C : Matrix n m R) (D : Matrix n n R) :
(Matrix.fromBlocks A 0 C D).det = A.det * D.det := by
rw [← det_transpose, fromBlocks_transpose, transpose_zero, det_fromBlocks_zero₂₁, det_transpose, det_transpose]
