det_one_sub_mul_comm — Mathlib

English

A corollary of Weinstein–Aronszajn: det(I − A B) = det(I − B A) for A and B of compatible sizes.

Русский

Следствие Леммы Вайнштейна–Аронзьяна: det(I − AB) = det(I − BA).

LaTeX

$$$\\det(I - A B) = \\det(I - B A)$$$

Lean4

theorem det_one_sub_mul_comm (A : Matrix m n α) (B : Matrix n m α) : det (1 - A * B) = det (1 - B * A) := by
  rw [sub_eq_add_neg, ← Matrix.neg_mul, det_one_add_mul_comm, Matrix.mul_neg, ← sub_eq_add_neg]

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