instHasBinaryBiproductObjEval

Mathlib.Algebra.Homology.HomologicalComplexBiprod

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instHasBinaryBiproductObjEval

English

There exists a binary biproduct in the evaluation at each index i.

Русский

Для каждого индекса i существует бинопроизводный объект в оценке.

LaTeX

$$$\\text{HasBinaryBiproduct}((\\mathrm{eval}\\; C\\; c\\; i)\\!\\!\\!\\!\\!\\!)$$$

Lean4

instance (i : ι) : HasBinaryBiproduct ((eval C c i).obj K) ((eval C c i).obj L) :=
  by
  dsimp [eval]
  infer_instance

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

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

Разделы

Аффилиация

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