det_mul_right_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_right_comm` applies under `det`. -/
theorem det_mul_right_comm (M N P : Matrix m m R) : det (M * N * P) = det (M * P * N) := by
  rw [Matrix.mul_assoc, Matrix.mul_assoc, det_mul, det_mul_comm N P, ← det_mul]
    -- TODO(https://github.com/leanprover-community/mathlib4/issues/6607): fix elaboration so `val` isn't needed

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