English
Two linear maps from Matrix m n α to β are equal if they agree on all singleLinearMap i j; i.e., extensionality along the standard basis for linear maps holds.
Русский
Два линейных отображения от матриц к β равны, если они совпадают на всех базисных линейных отображениях singleLinearMap i j.
LaTeX
$$$ f = g \; \Leftrightarrow \forall i,j, f \circ \mathrm{singleLinearMap}_{i j} = g \circ \mathrm{singleLinearMap}_{i j} $$$
Lean4
/-- Linear maps from finite matrices are equal if they agree on the standard basis.
See note [partially-applied ext lemmas]. -/
@[local ext]
theorem ext_linearMap [Finite m] [Finite n] [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β]
⦃f g : Matrix m n α →ₗ[R] β⦄ (h : ∀ i j, f ∘ₗ singleLinearMap R i j = g ∘ₗ singleLinearMap R i j) : f = g :=
LinearMap.toAddMonoidHom_injective <| ext_addMonoidHom fun i j => congrArg LinearMap.toAddMonoidHom <| h i j
