leftDerived_comp — Mathlib

English

LeftDerived respects composition: the leftDerived of the composite equals the composition of leftDeriveds.

Русский

Левый производный сохраняет композицию: левый производный композиции равен композиции левых производных.

LaTeX

$$$ \mathrm{leftDerived}(\alpha \circ \beta) = \mathrm{leftDerived}(\alpha) \circ \mathrm{leftDerived}(\beta) $$$

Lean4

@[simp, reassoc]
theorem leftDerived_comp {F G H : C ⥤ D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) :
    NatTrans.leftDerived (α ≫ β) n = NatTrans.leftDerived α n ≫ NatTrans.leftDerived β n := by
  simp [NatTrans.leftDerived]

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