English
Two R-linear maps φ and ψ from Π₀ i, M_i to N are equal if they agree on every single i via the maps sending x to single i x.
Русский
Два линейных отображения φ, ψ из Π₀ i, M_i в N равны, если они совпадают на каждом i через отображения, отправляющие x в single i x.
LaTeX
$$$\\forall φ, ψ : (Π_0 i, M_i) \\to_ℓ[R] N, \\; (\\forall i, x, φ(\\mathrm{single}(i,x)) = ψ(\\mathrm{single}(i,x))) \\Rightarrow φ = ψ$$$
Lean4
/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere. -/
theorem lhom_ext ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ (h : ∀ i x, φ (single i x) = ψ (single i x)) : φ = ψ :=
LinearMap.toAddMonoidHom_injective <| addHom_ext h
