cramer_smul — Mathlib

English

Scaling the matrix by a scalar r scales the Cramer map by r^{n-1}: cramer(rA) = r^{n-1} cramer(A).

Русский

Умножение матрицы на скаляр r масштабирует крамеровскую отображение: cramer(rA) = r^{n-1} cramer(A).

LaTeX

$$$$cramer(r \\cdot A) = r^{\\,Fintype.card\,n - 1} \\cdot cramer(A).$$$$

Lean4

theorem cramer_smul (r : α) (A : Matrix n n α) : cramer (r • A) = r ^ (Fintype.card n - 1) • cramer A :=
  LinearMap.ext fun _ => funext fun _ => det_updateCol_smul_left _ _ _ _

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