Solution_to_Simultaneous_Linear_Equations
Provedlinear-algebralinear-equationsmatrixproofwiki
Let be a system of simultaneous linear equations. where all of are elements of a field . Then is a solution of this system where is an matrix.
Preamble
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Formal statement
theorem Solution_to_Simultaneous_Linear_Equations {R : Type _} [Field R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) (b : Fin n → R) (hA : IsUnit A.det) : ∃! x : Fin n → R, A.mulVec x = b := by sorrySource