coe_zero

Mathlib.Analysis.Distribution.SchwartzSpace

URI: https://scilib.ai/kg/mathlib#SchwartzMap.coe_zero

English

The scalar action by 0 is the zero map, and its seminorms vanish.

Русский

Действие нуля на SchwartzMap даёт нулевую карту; её семинормы равны нулю.

LaTeX

$$$ (0) \\cdot f = 0 \\quad\\text{and}\\quad f.seminormAux_{k,n} \\text{ for } f=0$$$

Lean4

theorem coe_zero : DFunLike.coe (0 : 𝓢(E, F)) = (0 : E → F) :=
  rfl

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

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

Разделы

Аффилиация

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