English
The diagonal of a function d is the matrix with d(i) on the i-th diagonal entry and zeros elsewhere.
Русский
Диагональная матрица диагонализирует функцию d: d(i) на i-й диагонали, нули вне диагонали.
LaTeX
$$$\\nabla d:\\nabla diag(d) : \\; diag(d)_{ii} = d(i), \\ diag(d)_{ij} = 0 \\ (i \\neq j)$$$
Lean4
/-- `diagonal d` is the square matrix such that `(diagonal d) i i = d i` and `(diagonal d) i j = 0`
if `i ≠ j`.
Note that bundled versions exist as:
* `Matrix.diagonalAddMonoidHom`
* `Matrix.diagonalLinearMap`
* `Matrix.diagonalRingHom`
* `Matrix.diagonalAlgHom`
-/
def diagonal [Zero α] (d : n → α) : Matrix n n α :=
of fun i j =>
if i = j then d i
else
0
-- TODO: set as an equation lemma for `diagonal`, see https://github.com/leanprover-community/mathlib4/pull/3024
