English
For A with IsUnit det(A) and U,V of appropriate sizes, det(A + UV) = det(A) det(I + V A^{-1} U). This is a general Matrix determinant lemma variant.
Русский
Пусть det(A) обращает как единицу (IsUnit) и U,V подходящих размеров. Тогда det(A + UV) = det(A) det(I + V A^{-1} U).
LaTeX
$$$\\det(A + U V) = \\det(A) \\cdot \\det\\bigl(I + V A^{-1} U\\bigr) \\quad (\\text{with } IsUnit(\\det A))$$$
Lean4
/-- The **Matrix determinant lemma**
TODO: show the more general version without `hA : IsUnit A.det` as
`(A + replicateCol u * replicateRow v).det = A.det + v ⬝ᵥ (adjugate A) *ᵥ u`.
-/
theorem det_add_replicateCol_mul_replicateRow {ι : Type*} [Unique ι] {A : Matrix m m α} (hA : IsUnit A.det)
(u v : m → α) :
(A + replicateCol ι u * replicateRow ι v).det = A.det * (1 + replicateRow ι v * A⁻¹ * replicateCol ι u).det :=
by
nth_rewrite 1 [← Matrix.mul_one A]
rwa [← Matrix.mul_nonsing_inv_cancel_left A (replicateCol ι u * replicateRow ι v), ← Matrix.mul_add, det_mul, ←
Matrix.mul_assoc, det_one_add_mul_comm, ← Matrix.mul_assoc]
