opcyclesMap'_eq

Mathlib.Algebra.Homology.ShortComplex.Homology

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.HomologyMapData.opcyclesMap'_eq

English

Equality: opcyclesMap' φ h1.right h2.right = γ.right.φQ.

Русский

Равенство: opcyclesMap' φ h1.right h2.right = γ.right.φQ.

LaTeX

$$$opcyclesMap'\;φ\;h_1.right\;h_2.right = γ.right.φQ$$$

Lean4

theorem opcyclesMap'_eq : opcyclesMap' φ h₁.right h₂.right = γ.right.φQ :=
  RightHomologyMapData.congr_φQ (Subsingleton.elim _ _)

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

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

Разделы

Аффилиация

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