instHasZeroObjectLocalization' — Mathlib

English

If C has a zero object and W is a localization with left fractions, then the localized category W.Localization has a zero object.

Русский

Если в C есть нулевой объект, и W является локализацией с левыми дробями, то локализация W.Localization имеет нулевой объект.

LaTeX

$$\operatorname{HasZeroObject}(W.Localization)$$

Lean4

instance [HasZeroObject C] : HasZeroObject W.Localization' :=
  W.Q'.hasZeroObject_of_additive

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