diag — Mathlib

English

The diagonal of a square matrix A is the function that assigns to each index i the (i,i) entry of A.

Русский

Диагональ квадратной матрицы A — это отображение, которому каждому индексу i сопоставляет элемент A_{ii}.

LaTeX

$$$\mathrm{diag}(A) : n \to \alpha \quad\text{is defined by}\quad \mathrm{diag}(A)(i) = A_{ii}$$$

Lean4

/-- The diagonal of a square matrix. -/
def diag (A : Matrix n n α) (i : n) : α :=
  A i i

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