English
Additive maps from finite matrices are determined by their values on the standard basis: two AddMonoidHoms f,g: Matrix m n α →+ β are equal if for all i,j, f ∘ singleAddMonoidHom i j = g ∘ singleAddMonoidHom i j.
Русский
Аддитивные отображения из конечных матриц определяются по значениям на базисе: если для всех i,j выполняется равенство f ∘ singleAddMonoidHom i j = g ∘ singleAddMonoidHom i j, то f = g.
LaTeX
$$$ \forall i,j,\; f \circ \mathrm{singleAddMonoidHom}_{i j} = g \circ \mathrm{singleAddMonoidHom}_{i j} \Rightarrow f = g $$$
Lean4
/-- Additive maps from finite matrices are equal if they agree on the standard basis.
See note [partially-applied ext lemmas]. -/
@[local ext]
theorem ext_addMonoidHom [Finite m] [Finite n] [AddCommMonoid α] [AddCommMonoid β] ⦃f g : Matrix m n α →+ β⦄
(h : ∀ i j, f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)) : f = g :=
by
cases nonempty_fintype m
cases nonempty_fintype n
ext x
rw [matrix_eq_sum_single x]
simp_rw [map_sum]
congr! 2
exact DFunLike.congr_fun (h _ _) _
