det_smul — Mathlib

English

If a matrix is multiplied by a scalar c, its determinant is scaled by c raised to the dimension: det(cA) = c^n det(A).

Русский

Умножение матрицы на скаляр c масштабирует детерминант на c^n, где n — размер матрицы.

LaTeX

$$$$\det(cA) = c^{n} \det A,$$ где $n$ — размер матрицы $A$.$$

Lean4

theorem det_smul (A : Matrix n n R) (c : R) : det (c • A) = c ^ Fintype.card n * det A :=
  calc
    det (c • A) = det ((diagonal fun _ => c) * A) := by rw [smul_eq_diagonal_mul]
    _ = det (diagonal fun _ => c) * det A := (det_mul _ _)
    _ = c ^ Fintype.card n * det A := by simp

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