matrix_apply — Mathlib

English

Applying the standard basis matrix to a basis element gives the corresponding elementary matrix.

Русский

Применение элемента базиса к стандартной матрице даёт соответствующую элементарную матрицу.

LaTeX

$$$\\\\text{Basis}.matrix(m,n,b) (i,j,k) = E_{i j} \\\\text{(with entry } b(k) )$$$

Lean4

@[simp]
theorem matrix_apply (b : Basis ι R M) (i : m) (j : n) (k : ι) [DecidableEq m] [DecidableEq n] :
    b.matrix m n (i, j, k) = Matrix.single i j (b k) := by simp [Basis.matrix, Matrix.single_eq_of_single_single]

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