det_units_conj — Mathlib

English

Let M be invertible and N any square matrix over a commutative ring R. Then det(M N M^{-1}) = det N.

Русский

Пусть M — обратимая квадратная матрица над R, и N — любая квадратная матрица. Тогда det(M N M^{-1}) = det N.

LaTeX

$$$$\det(M N M^{-1}) = \det N$$$$

Lean4

theorem det_units_conj (M : (Matrix m m R)ˣ) (N : Matrix m m R) : det (M.val * N * M⁻¹.val) = det N := by
  rw [det_mul_right_comm, Units.mul_inv, one_mul]
    -- TODO(https://github.com/leanprover-community/mathlib4/issues/6607): fix elaboration so `val` isn't needed

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