English
If φ and ψ satisfy φ ∘ lsingle i = ψ ∘ lsingle i for every i, then φ = ψ.
Русский
Если для каждого i выполнено φ ∘ lsingle i = ψ ∘ lsingle i, то φ = ψ.
LaTeX
$$$(\\forall i, φ \\circ \\mathrm{lsingle}(i) = ψ \\circ \\mathrm{lsingle}(i)) \\Rightarrow φ = ψ$$$
Lean4
/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere.
See note [partially-applied ext lemmas].
After applying this lemma, if `M = R` then it suffices to verify
`φ (single a 1) = ψ (single a 1)`. -/
@[ext 1100]
theorem lhom_ext' ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ (h : ∀ i, φ.comp (lsingle i) = ψ.comp (lsingle i)) : φ = ψ :=
lhom_ext fun i => LinearMap.congr_fun (h i)
