instInjectiveXNatOfCocomplex

Mathlib.CategoryTheory.Abelian.Injective.Resolution

URI: https://scilib.ai/kg/mathlib#CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex

English

For each n, the nth object in the constructed cocomplex is injective.

Русский

Для каждого n объект кококомплекса является инъективным.

LaTeX

$$Injective ((ofCocomplex Z).X n) $$

Lean4

instance (n : ℕ) : Injective ((ofCocomplex Z).X n) := by obtain (_ | _ | _ | n) := n <;> apply Injective.injective_under

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

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

Разделы

Аффилиация

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