ρ₁₂

Mathlib.Algebra.Homology.ComplexShapeSigns

URI: https://scilib.ai/kg/mathlib#ComplexShape.ρ₁₂

Lean4

/-- The `GradedObject.BifunctorComp₁₂IndexData` which arises from complex shapes. -/
@[reducible]
def ρ₁₂ : GradedObject.BifunctorComp₁₂IndexData (r c₁ c₂ c₃ c₁₂ c)
    where
  I₁₂ := I₁₂
  p := π c₁ c₂ c₁₂
  q := π c₁₂ c₃ c
  hpq _ := rfl

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

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

Разделы

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

Аффилиация

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