instIsClosedUnderExtensionsIsZero

Mathlib.CategoryTheory.ObjectProperty.Extensions

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsIsZero

← MathLib Explorer

English

IsZero is closed under extensions.

Русский

IsZero замкнуто по расширениям.

LaTeX

$$$\text{IsClosedUnderExtensions}(\mathrm{IsZero}(C)).$$$

Lean4

instance : IsClosedUnderExtensions (IsZero (C := C)) where
  prop_X₂_of_shortExact hS h₁ h₃ := hS.exact.isZero_of_both_zeros (h₁.eq_of_src _ _) (h₃.eq_of_tgt _ _)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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