English
There exists a linear operator cramer : (n→α) → (n→α) defined by cramer A, which computes the Cramer's rule vector for A and any b.
Русский
Существует линейный оператор cramer: (α^n) → (α^n), который для заданной матрицы A возвращает вектор по правилу Крамера.
LaTeX
$$$$cramer : (\\mathbb{n} \\to \\alpha) \\to (\\mathbb{n} \\to \\alpha) \\text{ is linear and equals the map } b \\mapsto cramerMap A b.$$$$
Lean4
/-- `cramer A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,
and thus `cramer A b` is the vector output by Cramer's rule on `A` and `b`.
If `A * x = b` has a unique solution in `x`, `cramer A` sends the vector `b` to `A.det • x`.
Otherwise, the outcome of `cramer` is well-defined but not necessarily useful.
-/
def cramer (A : Matrix n n α) : (n → α) →ₗ[α] (n → α) :=
IsLinearMap.mk' (cramerMap A) (cramer_is_linear A)
