adjugate_smul — Mathlib

English

If a matrix A is scaled by a scalar r, then adjugate scales by r^(n−1): adj(rA) = r^{n−1} adj(A).

Русский

Если матрица A масштабируется на скаляра r, то adjugate масштабируется на r^{n−1}: adj(rA) = r^{n−1} adj(A).

LaTeX

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

Lean4

theorem adjugate_smul (r : α) (A : Matrix n n α) : adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A :=
  by
  rw [adjugate, adjugate, transpose_smul, cramer_smul]
  rfl

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