map_intCast — Mathlib

English

For AddGroupWithOne α and Zero β, mapping an integer d to a diagonal yields the diagonal of d.cast.

Русский

Для AddGroupWithOne α и Zero β отображение целого числа d в диагональ даёт диагональ с d.cast.

LaTeX

$$$[AddGroupWithOne α] [Zero β] {f : α \to β}, (\text{f 0} = 0) \Rightarrow \forall (d : \mathbb{Z}), (d.cast.map f) = \mathrm{diagonal}(f(d.cast))$$$

Lean4

protected theorem map_intCast [AddGroupWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℤ) :
    (d : Matrix n n α).map f = diagonal (fun _ => f d) :=
  diagonal_map h

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