English
For a fixed matrix A and vector b, the i-th component of cramerMap A b is the determinant of the matrix A with its i-th column replaced by b.
Русский
Пусть A — матрица размера n×n над кольцом α, а b ∈ α^n. Тогда i-й компонент cramerMap A b равен детерминанту матрицы A с заменённым i‑м столбцом на b.
LaTeX
$$$$\\text{cramerMap}(i) = \\det\\bigl(A\\text{ with column } i \\text{ replaced by } b\\bigr).$$$$
Lean4
/-- `cramerMap A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,
and thus `cramerMap A b` is the vector output by Cramer's rule on `A` and `b`.
If `A * x = b` has a unique solution in `x`, `cramerMap A` sends the vector `b` to `A.det • x`.
Otherwise, the outcome of `cramerMap` is well-defined but not necessarily useful.
-/
def cramerMap (i : n) : α :=
(A.updateCol i b).det
