linearMap_ext — Mathlib

English

The linear equivalence sends the component inclusion loaf to the standard delta function Pi.single i m.

Русский

Линейное эквивалентное отображение переводит включение компоненты с lof в обычную дельта-функцию Pi.single i m.

LaTeX

$$$ (linearEquivFunOnFintype\\; R\\; ι\\; M)\; (\\mathrm{lof}\\; R\\; ι\\; M\\; i\\; m) = \\mathrm{Pi.single}\\; i\\; m $$$

Lean4

/-- Two `LinearMap`s out of a direct sum are equal if they agree on the generators.

See note [partially-applied ext lemmas]. -/
@[ext]
theorem linearMap_ext ⦃ψ ψ' : (⨁ i, M i) →ₗ[R] N⦄ (H : ∀ i, ψ.comp (lof R ι M i) = ψ'.comp (lof R ι M i)) : ψ = ψ' :=
  DFinsupp.lhom_ext' H

Похожие утверждения