mulVec_cramer — Mathlib

English

If the index set is a singleton, then adjugate A = I.

Русский

Если множество индексов единичное, то adjugate A = I.

LaTeX

$$$\operatorname{adj}(A) = I_n$ \text{ when } |n| = 1$$

Lean4

/-- A stronger form of **Cramer's rule** that allows us to solve some instances of `A * x = b` even
if the determinant is not a unit. A sufficient (but still not necessary) condition is that `A.det`
divides `b`. -/
@[simp]
theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A *ᵥ cramer A b = A.det • b := by
  rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]

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