charpoly_mul_comm — Mathlib

English

Let A and B be square matrices of size n over a commutative ring. Then the characteristic polynomials of AB and BA are equal.

Русский

Пусть A и B — квадратные матрицы размера n над коммутативной кольцом. Тогда характеристические многочлены AB и BA совпадают.

LaTeX

$$$$ \\operatorname{charpoly}(AB) = \\operatorname{charpoly}(BA). $$$$

Lean4

/-- A version of `charpoly_mul_comm'` for square matrices. -/
theorem charpoly_mul_comm (A B : Matrix n n R) : (A * B).charpoly = (B * A).charpoly :=
  (isRegular_X_pow _).left.eq_iff.mp <| charpoly_mul_comm' A B

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