shiftFunctorAdd_eq — Mathlib

English

ShiftFunctorAdd on Triangle C agrees with the generic ShiftFunctorAdd' construction.

Русский

ShiftFunctorAdd на Triangle C совпадает с общей конструкцией ShiftFunctorAdd'.

LaTeX

$$$\\operatorname{shiftFunctorAdd}(\\operatorname{Triangle} C) a b = \\operatorname{Triangle.shiftFunctorAdd'} C a b (a+b) \\cdots$$$

Lean4

@[simp]
theorem shiftFunctorAdd_eq (a b : ℤ) :
    CategoryTheory.shiftFunctorAdd (Triangle C) a b = Triangle.shiftFunctorAdd' C a b _ rfl :=
  ShiftMkCore.shiftFunctorAdd_eq _ _ _

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