shiftFunctor_eq — Mathlib

English

The shift functor addition on Triangle C coincides with the canonical Triangle shiftFunctorAdd' construction.

Русский

Сложение сдвигов на Triangle C совпадает с канонической конструкцией shiftFunctorAdd' на треугольниках.

LaTeX

$$$\\operatorname{shiftFunctorAdd}(\\operatorname{Triangle} C) a b = \\operatorname{Triangle.shiftFunctorAdd'} C a b (a+b) \\;\\text{(with proof)}$$$

Lean4

@[simp]
theorem shiftFunctor_eq (n : ℤ) : CategoryTheory.shiftFunctor (Triangle C) n = Triangle.shiftFunctor C n :=
  rfl

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