English
Let f: α → β satisfy f(0) = 0 and f(1) = 1. Then applying f entrywise to the n×n identity matrix yields the n×n identity matrix over β: (I_n(α)) map f = I_n(β).
Русский
Пусть f: α → β удовлетворяет f(0) = 0 и f(1) = 1. Тогда поэлементное применение f к квадратной единичной матрице даёт квадратную единичную матрицу над β: I_n(α)map f = I_n(β).
LaTeX
$$$\bigl(f(0)=0\bigr) \land \bigl(f(1)=1\bigr) \implies (1 : \mathrm{Matrix}\ n\ n\ α).\mathrm{map}\ f = (1 : \mathrm{Matrix}\ n\ n\ β)$$$
Lean4
@[simp]
protected theorem map_one [Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
(1 : Matrix n n α).map f = (1 : Matrix n n β) := by
ext
simp only [one_apply, map_apply]
split_ifs <;> simp [h₀, h₁]
