cramerMap_is_linear — Mathlib

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 _ _ }

Похожие утверждения