instHasProjectiveDimensionLTHAddNat_1

Mathlib.CategoryTheory.Abelian.Projective.Dimension

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

English

If HasProjectiveDimensionLT X n holds, then HasProjectiveDimensionLT X n.succ holds.

Русский

Если HasProjectiveDimensionLT X n, то HasProjectiveDimensionLT X n.succ.

LaTeX

$$$ [\text{HasProjectiveDimensionLT } X n] \Rightarrow [\text{HasProjectiveDimensionLT } X (n+1)]. $$$

Lean4

instance [HasProjectiveDimensionLT X n] (k : ℕ) : HasProjectiveDimensionLT X (k + n) :=
  hasProjectiveDimensionLT_of_ge X n (k + n) (by cutsat)

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

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

Разделы

Аффилиация

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