English
If the index type m is unique and zero element exists, the diagonal determined by d equals the constant matrix with value d(default) everywhere.
Русский
Если индексный тип m уникален и существует нулевой элемент, диагональ, заданная d, равна константной матрице со значением d(default) во всех позициях.
LaTeX
$$$[Unique m] [DecidableEq m] [Zero \alpha] (d : m \to \alpha) : \mathrm{diagonal}(d) = \mathrm{of}(\lambda _ _ \mapsto d(\mathrm{default}))$$$
Lean4
theorem diagonal_unique [Unique m] [DecidableEq m] [Zero α] (d : m → α) : diagonal d = of fun _ _ => d default :=
by
ext i j
rw [Subsingleton.elim i default, Subsingleton.elim j default, diagonal_apply_eq _ _, of_apply]
