det_smul_inv_mulVec_eq_cramer — Mathlib

English

A form of Cramer's rule: det(A) times A^{-1} times b equals the Cramer vector for b, i.e., det(A) A^{-1} b = cramer(A,b) when det(A) is a unit.

Русский

Форма правила Крамера: det(A) A^{-1} b = cramer(A,b) при det(A) единица (или когда A обратима).

LaTeX

$$A.det • A^{-1} *ᵥ b = cramer A b$$

Lean4

/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/
@[simp]
theorem det_smul_inv_mulVec_eq_cramer (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
    A.det • A⁻¹ *ᵥ b = cramer A b := by
  rw [cramer_eq_adjugate_mulVec, A.nonsing_inv_apply h, ← smul_mulVec, smul_smul, h.mul_val_inv, one_smul]

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