English
For any A and b, cramer A b equals A.adjugate times the vector b, i.e., cramer A b = A.adjugate ·ᵥ b.
Русский
Для любой A и b выполняется cramer A b = A.adjugate умноженное на вектор b, т.е. cramer A b = A.adjugate ·ᵥ b.
LaTeX
$$$$\\mathrm{cramer}(A,b) = A\\adjugate \\cdot\\!\\mathbf{b}.$$$
Lean4
/-- Since the map `b ↦ cramer A b` is linear in `b`, it must be multiplication by some matrix. This
matrix is `A.adjugate`. -/
theorem cramer_eq_adjugate_mulVec (A : Matrix n n α) (b : n → α) : cramer A b = A.adjugate *ᵥ b :=
by
nth_rw 2 [← A.transpose_transpose]
rw [← adjugate_transpose, adjugate_def]
have : b = ∑ i, b i • (Pi.single i 1 : n → α) :=
by
refine (pi_eq_sum_univ b).trans ?_
congr with j
simp [Pi.single_apply, eq_comm]
conv_lhs => rw [this]
ext k
simp [mulVec, dotProduct, mul_comm]
