val_single — Mathlib

English

The underlying matrix of the linear map single(i,j,h) applied to r is exactly the standard matrix unit E_{ij} scaled by r.

Русский

Пусть выполняется, что подлежащая матрица элемента линейного отображения single(i,j,h) при действии на r равна стандартной матрице-единице E_{ij}, умноженной на r.

LaTeX

$$$$ (single\, i\, j\, h\, r).\text{val} = \mathrm{Matrix.single}_{i j} \ r. $$$$

Lean4

@[simp]
theorem val_single (h : i ≠ j) (r : R) : (single i j h r).val = Matrix.single i j r :=
  rfl

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