isIso_leftHomologyπ

Mathlib.Algebra.Homology.ShortComplex.LeftHomology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.isIso_leftHomologyπ

English

If S.f = 0, then leftHomologyπ is an isomorphism.

Русский

Если S.f = 0, то leftHomologyπ является изоморфизмом.

LaTeX

$$$ S.f = 0 \\Rightarrow IsIso(S.leftHomologyπ) $$$

Lean4

theorem isIso_leftHomologyπ (hf : S.f = 0) : IsIso S.leftHomologyπ :=
  LeftHomologyData.isIso_π _ hf

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

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

Разделы

Аффилиация

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