map — Mathlib

English

Let A be a diagonal square matrix over α. If f: α → β satisfies f(0) = 0, then applying f entrywise to A yields a diagonal matrix over β.

Русский

Пусть A — диагональная квадратная матрица над α. Пусть f: α → β удовлетворяет f(0) = 0. Тогда применение f по каждому элементу к A даёт диагональную матрицу над β.

LaTeX

$$$\\forall {\\alpha ⁢ {\\beta}} [Zero \\a] [Zero \\beta] {A : Matrix \\n n \\ n \\a}, A.IsDiag \\to \\forall f : \\a \\to \\beta, f(0) = 0 \\to (A.map f).IsDiag$$$

Lean4

theorem map [Zero α] [Zero β] {A : Matrix n n α} (ha : A.IsDiag) {f : α → β} (hf : f 0 = 0) : (A.map f).IsDiag :=
  by
  intro i j h
  simp [ha h, hf]

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