det_one_add_mul_comm — Mathlib

English

For rectangular A (m×n) and B (n×m), the determinants satisfy det(I_m + A B) = det(I_n + B A).

Русский

Для прямоугольных матриц A (m×n) и B (n×m) выполняется det(I_m + A B) = det(I_n + B A).

LaTeX

$$$\\det(I_m + A B) = \\det(I_n + B A)$$$

Lean4

/-- The **Weinstein–Aronszajn identity**. Note the `1` on the LHS is of shape m×m, while the `1` on
the RHS is of shape n×n. -/
theorem det_one_add_mul_comm (A : Matrix m n α) (B : Matrix n m α) : det (1 + A * B) = det (1 + B * A) :=
  calc
    det (1 + A * B) = det (fromBlocks 1 (-A) B 1) := by rw [det_fromBlocks_one₂₂, Matrix.neg_mul, sub_neg_eq_add]
    _ = det (1 + B * A) := by rw [det_fromBlocks_one₁₁, Matrix.mul_neg, sub_neg_eq_add]

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