instHasInjectiveDimensionLTOfNatNat

Mathlib.CategoryTheory.Abelian.Injective.Dimension

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instHasInjectiveDimensionLTOfNatNat

English

There is an instance HasInjectiveDimensionLT X n for all n, given HasInjectiveDimensionLT X 0.

Русский

Для каждого n существует инстанс HasInjectiveDimensionLT X n, если задан HasInjectiveDimensionLT X 0.

LaTeX

$$$\text{HasInjectiveDimensionLT}(X,n)$ для всех n по инстансу$$

Lean4

instance : HasInjectiveDimensionLT (0 : C) 0 :=
  (isZero_zero C).hasInjectiveDimensionLT_zero

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

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

Разделы

Аффилиация

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