shiftFunctorAdd'_eq — Mathlib

English

Equality between shiftFunctorAdd' computed for Triangle C and the base shiftFunctorAdd'.

Русский

Равенство между computed shiftFunctorAdd' для Triangle C и базовым shiftFunctorAdd'.

LaTeX

$$$\\operatorname{shiftFunctorAdd'} (\\operatorname{Triangle} C) a b c h = \\operatorname{Triangle.shiftFunctorAdd'} C a b c h$$$

Lean4

@[simp]
theorem shiftFunctorAdd'_eq (a b c : ℤ) (h : a + b = c) :
    CategoryTheory.shiftFunctorAdd' (Triangle C) a b c h = Triangle.shiftFunctorAdd' C a b c h :=
  by
  subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd]
  apply shiftFunctorAdd_eq

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