isZero_of_isGE

Mathlib.Algebra.Homology.Embedding.CochainComplex

URI: https://scilib.ai/kg/mathlib#CochainComplex.isZero_of_isGE

English

If K.IsGE n and K.HasHomology i, then the homology at i vanishes: IsZero(K.homology i).

Русский

Если K.IsGE n и у K есть гомология в степени i, то H^i(K) = 0.

LaTeX

$$IsZero(K.homology i)$$

Lean4

theorem isZero_of_isGE (n i : ℤ) (hi : i < n) [K.IsGE n] [K.HasHomology i] : IsZero (K.homology i) :=
  (K.exactAt_of_isGE n i hi).isZero_homology

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

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

Разделы

Аффилиация

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