localization_zero

Mathlib.CategoryTheory.Center.Localization

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatCenter.localization_zero

English

Localization preserves zero: (0 : CatCenter C).localization L W = 0.

Русский

Локализация сохраняет ноль: локализация 0 равна 0.

LaTeX

$$$0_{\!\text{CatCenter C}}.localization\; L\; W = 0_{\!\text{CatCenter D}}$$$

Lean4

theorem localization_zero : (0 : CatCenter C).localization L W = 0 :=
  ext_of_localization L W _ _ (fun X => by simp)

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

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

Разделы

Аффилиация

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