det_conj_of_mul_eq_one — Mathlib

English

If M M' = 1 and M' M = 1, then det(M N M') = det N.

Русский

Если M M' = 1 и M' M = 1, то det(M N M') = det N.

LaTeX

$$det (M * N * M') = det N$$

Lean4

/-- If `M'` is a two-sided inverse for `M` (indexed differently), `det (M * N * M') = det N`.

See `Matrix.det_conj` and `Matrix.det_conj'` for the case when `M' = M⁻¹` or vice versa. -/
theorem det_conj_of_mul_eq_one [DecidableEq m] [DecidableEq n] {M : Matrix m n A} {M' : Matrix n m A} {N : Matrix n n A}
    (hMM' : M * M' = 1) (hM'M : M' * M = 1) : det (M * N * M') = det N := by
  rw [← det_comm' hM'M hMM', ← Matrix.mul_assoc, hM'M, Matrix.one_mul]

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