diagonal_map — Mathlib

English

Let f be a function with f(0) = 0. Then mapping a diagonal matrix by f yields the diagonal of the mapped entries.

Русский

Пусть f такова, что f(0) = 0. Тогда отображение диагональной матрицы через f эквивалентно диагонали от значений f(diagonal).

LaTeX

$$$f(0)=0 \Rightarrow (\mathrm{diagonal}(d)).map f = \mathrm{diagonal}(f\circ d)$$$

Lean4

@[simp]
theorem diagonal_map [Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} :
    (diagonal d).map f = diagonal fun m => f (d m) := by
  ext
  simp only [diagonal_apply, map_apply]
  split_ifs <;> simp [h]

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