English
A general form of the matrix determinant lemma: det(A + UV) = det(A) det(I + V A^{-1} U) whenever A is invertible in the determinant sense (or is unit).
Русский
Общая форма леммы детерминанта для матриц: det(A + UV) = det(A) det(I + V A^{-1} U), если A обратима (детерминант является единицей).
LaTeX
$$$\\det(A + U V) = \\det(A) \\cdot \\det\\bigl(I + V A^{-1} U\\bigr) \\quad \\text{(with invertible } A)$$$
Lean4
/-- A generalization of the **Matrix determinant lemma** -/
theorem det_add_mul {A : Matrix m m α} (U : Matrix m n α) (V : Matrix n m α) (hA : IsUnit A.det) :
(A + U * V).det = A.det * (1 + V * A⁻¹ * U).det :=
by
nth_rewrite 1 [← Matrix.mul_one A]
rwa [← Matrix.mul_nonsing_inv_cancel_left A (U * V), ← Matrix.mul_add, det_mul, ← Matrix.mul_assoc,
det_one_add_mul_comm, ← Matrix.mul_assoc]
