cramer_is_linear — Mathlib

English

For a fixed matrix A, the map b ↦ cramer A b is a linear map; i.e., cramer A defines a linear transformation on vectors b ∈ α^n.

Русский

Для фиксированной матрицы A отображение b ↦ cramer A b является линейным преобразованием на векторах b ∈ α^n.

LaTeX

$$$$\\text{cramer A is linear: } cramer A : (\\alpha^n) \\to (\\alpha^n)\\text{ is an } \\alpha\\text{-linear map}.$$$$

Lean4

theorem cramer_is_linear : IsLinearMap α (cramerMap A) :=
  by
  constructor <;> intros <;> ext i
  · apply (cramerMap_is_linear A i).1
  · apply (cramerMap_is_linear A i).2

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