English
Let φ, ψ be R-linear maps from Finsupp X M to N. If for every a, φ ∘ lsingle a = ψ ∘ lsingle a, then φ = ψ. This is a version of extensionality using the coordinate projections lsingle a.
Русский
Пусть φ, ψ — R-линейные отображения из Finsupp X M в N. Если для каждого a выполняется φ ∘ lsingle a = ψ ∘ lsingle a, то φ = ψ. Это версия экстенсиональности с использованием координатных проекций.
LaTeX
$$$\\forall a: \\alpha,\\; φ\\circ (lsingle\,a)=ψ\\circ (lsingle\,a) \\Rightarrow φ=ψ$$$
Lean4
/-- Two `R`-linear maps from `Finsupp X M` which agree on each `single x y` agree everywhere.
We formulate this fact using equality of linear maps `φ.comp (lsingle a)` and `ψ.comp (lsingle a)`
so that the `ext` tactic can apply a type-specific extensionality lemma to prove equality of these
maps. E.g., if `M = R`, then it suffices to verify `φ (single a 1) = ψ (single a 1)`. -/
-- The priority should be higher than `LinearMap.ext`.
@[ext high]
theorem lhom_ext' ⦃φ ψ : (α →₀ M) →ₛₗ[σ₁₂] N⦄ (h : ∀ a, φ.comp (lsingle a) = ψ.comp (lsingle a)) : φ = ψ :=
lhom_ext fun a => LinearMap.congr_fun (h a)
