English
For a fixed matrix A, and for each i, the map b ↦ cramerMap A b i is a linear functional; i.e., the i-th coordinate of cramerMap A b depends linearly on b.
Русский
Для фиксированной матрицы A, для каждого i: отображение b ↦ cramerMap A b i является линейным функционалом; i‑й компонент крамерового отображения линейно зависит от b.
LaTeX
$$$$\\text{The map } b \\mapsto \\bigl(cramerMap\_A\, b\\bigr)\_i \\text{ is linear in } b$$$$
Lean4
theorem cramerMap_is_linear (i : n) : IsLinearMap α fun b => cramerMap A b i :=
{ map_add := det_updateCol_add _ _
map_smul := det_updateCol_smul _ _ }