lmapDomain_id

Mathlib.LinearAlgebra.Finsupp.Defs

URI: https://scilib.ai/kg/mathlib#Finsupp.lmapDomain_id

English

The application of lsingle a to b yields the singleton function with value b at a, i.e., (lsingle a) b = single a b.

Русский

Применение lsingle к a и b даёт базисный элемент: (lsingle a) b = single a b.

LaTeX

$$$lsingle\\ a : M \\to α\\to_0 M\\; b = single\\ a\\ b$$$

Lean4

@[simp]
theorem lmapDomain_id : (lmapDomain M R _root_.id : (α →₀ M) →ₗ[R] α →₀ M) = LinearMap.id :=
  LinearMap.ext fun _ => mapDomain_id

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru