val_singleSubSingle — Mathlib

English

A difference of two basis elements across a triple equals the remaining basis element: singleSubSingle i k r - singleSubSingle i j r = singleSubSingle j k r.

Русский

Разность двух базисных элементов по тройке индексов равна оставшемуся базисному элементу: singleSubSingle i k r - singleSubSingle i j r = singleSubSingle j k r.

LaTeX

$$$$ singleSubSingle(i,k,r) - singleSubSingle(i,j,r) = singleSubSingle(j,k,r). $$$$

Lean4

@[simp]
theorem val_singleSubSingle (r : R) : (singleSubSingle i j r).val = Matrix.single i i r - Matrix.single j j r :=
  rfl

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