English
If f(0) = 0 and d is a natural number, then applying f to the diagonal of d yields a diagonal with f(d) on the diagonal.
Русский
Если f(0)=0 и d — натуральное число, то отображение f диагонали d даёт диагональ с f(d) на диагонали.
LaTeX
$$$f(0)=0 \Rightarrow (d : Matrix n n \alpha).map f = \mathrm{diagonal}(\lambda _ . f(d))$$$
Lean4
protected theorem map_natCast [AddMonoidWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℕ) :
(d : Matrix n n α).map f = diagonal (fun _ => f d) :=
diagonal_map h