hasLeftHomology_of_hasHomology

Mathlib.Algebra.Homology.ShortComplex.Homology

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

English

If S has Homology, then S has a LeftHomology structure.

Русский

Если у S есть гомология, то у S есть левая гомология.

LaTeX

$$$HasLeftHomology(S)$$$

Lean4

instance hasLeftHomology_of_hasHomology [S.HasHomology] : S.HasLeftHomology :=
  HasLeftHomology.mk' S.homologyData.left

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

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

Разделы

Аффилиация

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