English
The sum of two basis elements corresponding to consecutive indices collapses to the third basis element: singleSubSingle i j r + singleSubSingle j k r = singleSubSingle i k r.
Русский
Сумма двух базисных элементов по соседним парам индексов дает третий элемент: singleSubSingle i j r + singleSubSingle j k r = singleSubSingle i k r.
LaTeX
$$$$ singleSubSingle(i,j,r) + singleSubSingle(j,k,r) = singleSubSingle(i,k,r). $$$$
Lean4
/-- The matrices with matching positive and negative elements on the diagonal are elements of
`sl n R`. Along with `single`, a subset of these form a basis for `sl n R`. -/
def singleSubSingle : R →ₗ[R] sl n R :=
LinearMap.codRestrict _ (Matrix.singleLinearMap R i i - Matrix.singleLinearMap R j j) fun r =>
LinearMap.sub_mem_ker_iff.mpr <| by simp
