isZero_of_isLE

Mathlib.Algebra.Homology.Embedding.CochainComplex

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

English

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

Русский

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

LaTeX

$$IsZero(K.homology i)$$

Lean4

theorem isZero_of_isLE (n i : ℤ) (hi : n < i) [K.IsLE n] [K.HasHomology i] : IsZero (K.homology i) :=
  (K.exactAt_of_isLE n i hi).isZero_homology

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

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

Разделы

Аффилиация

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