det_mul_left_comm — Mathlib

English

Let M,N,P be square matrices over a commutative ring R. Then det(M(NP)) = det(N(MP)).

Русский

Пусть M,N,P — квадратные матрицы над коммутативной кольцевой R. Тогда det(M(NP)) = det(N(MP)).

LaTeX

$$$$\det(M(NP)) = \det(N(MP))$$$$

Lean4

/-- On square matrices, `mul_left_comm` applies under `det`. -/
theorem det_mul_left_comm (M N P : Matrix m m R) : det (M * (N * P)) = det (N * (M * P)) := by
  rw [← Matrix.mul_assoc, ← Matrix.mul_assoc, det_mul, det_mul_comm M N, ← det_mul]

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