stdBasis_eq_single — Mathlib

English

The basis element corresponding to (i,j) equals the matrix with a single 1 at position (i,j).

Русский

Элемент базиса, соответствующий (i,j), равен матрице с единственной единицей на позиции (i,j).

LaTeX

$$$\\text{stdBasis}(R,m,n) (i,j) = E_{i j}$$$

Lean4

theorem stdBasis_eq_single (i : m) (j : n) [DecidableEq m] [DecidableEq n] :
    stdBasis R m n (i, j) = single i j (1 : R) := by simp [stdBasis, single_eq_of_single_single]

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