det_mul_add_one_comm — Mathlib

English

For A (m×n) and B (n×m), the identity det(AB + I) = det(BA + I) holds after appropriate rearrangements; this is an alternate formulation of Weinstein–Aronszajn.

Русский

Для A (m×n) и B (n×m) верна аналогичная формулировка детерминанта: det(AB + I) = det(BA + I).

LaTeX

$$$\\det(AB + I) = \\det(BA + I) \\quad \\text{with } A \\in M_{m\\times n}, B \\in M_{n\\times m}$$$

Lean4

/-- Alternate statement of the **Weinstein–Aronszajn identity** -/
theorem det_mul_add_one_comm (A : Matrix m n α) (B : Matrix n m α) : det (A * B + 1) = det (B * A + 1) := by
  rw [add_comm, det_one_add_mul_comm, add_comm]

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