English
For an additive monoid with one and a zero, mapping from ofNat(d) yields a diagonal with f(ofNat(d)) on the diagonal.
Русский
Для дополняющего моноида с единицей и нулём отображение from ofNat(d) даёт диагональ с f(ofNat(d)) на диагонали.
LaTeX
$$$[AddMonoidWithOne \alpha] [Zero \beta] {f : \alpha \to \beta}, (f 0 = 0) \Rightarrow \forall d, (\text{ofNat}(d) : Matrix n n \alpha).map f = \mathrm{diagonal}(\lambda x \to f(\text{ofNat}(d)))$$$
Lean4
protected theorem map_ofNat [AddMonoidWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] :
(ofNat(d) : Matrix n n α).map f = diagonal (fun _ => f (OfNat.ofNat d)) :=
diagonal_map h
