det_smul_inv_vecMul_eq_cramer_transpose

English

A form of Cramer's rule using transpose: det(A) times b transposed multiplied by A^{-1} equals cramer of A^T with b.

Русский

Форма правила Крамера через транспонирование: det(A) b^T A^{-1} = cramer(A^T,b).

LaTeX

$$det_smul_inv_vecMul_eq_cramer_transpose (A) (b) (h) : A.det • b ᵥ* A⁻¹ = cramer Aᵀ b$$

Lean4

/-- One form of **Cramer's rule**. See `Matrix.mulVec_cramer` for a stronger form. -/
@[simp]
theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
    A.det • b ᵥ* A⁻¹ = cramer Aᵀ b := by
  rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
    Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]

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