det_toMatrix_eq_det_toMatrix — Mathlib

English

A variant form of det_conj_of_mul_eq_one under different indexing conventions.

Русский

Вариант формы det_conj_of_mul_eq_one при другой индексации.

LaTeX

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

Lean4

/-- The determinant of `LinearMap.toMatrix` does not depend on the choice of basis. -/
theorem det_toMatrix_eq_det_toMatrix [DecidableEq κ] (b : Basis ι A M) (c : Basis κ A M) (f : M →ₗ[A] M) :
    det (LinearMap.toMatrix b b f) = det (LinearMap.toMatrix c c f) := by
  rw [← linearMap_toMatrix_mul_basis_toMatrix c b c, ← basis_toMatrix_mul_linearMap_toMatrix b c b,
      Matrix.det_conj_of_mul_eq_one] <;>
    rw [Basis.toMatrix_mul_toMatrix, Basis.toMatrix_self]

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