zero_completion

Mathlib.Analysis.Normed.Group.HomCompletion

URI: https://scilib.ai/kg/mathlib#NormedAddGroupHom.zero_completion

English

The completion of the zero map is the zero map: (0).completion = 0.

Русский

Завершение нулевого отображения равно нулю: 0^{comp} = 0.

LaTeX

$$$ (0 : \mathrm{NormedAddGroupHom} G H).\mathrm{completion} = 0.$$$

Lean4

@[simp]
theorem zero_completion : (0 : NormedAddGroupHom G H).completion = 0 :=
  normedAddGroupHomCompletionHom.map_zero

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

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

Разделы

Аффилиация

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