rightHomologyMapData

Mathlib.Algebra.Homology.ShortComplex.RightHomology

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

Lean4

/-- The (unique) right homology map data associated to a morphism of short complexes that
are both equipped with right homology data. -/
def rightHomologyMapData : RightHomologyMapData φ h₁ h₂ :=
  default

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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