map_natCast — Mathlib

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

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