instDecidableEqOrderedFinpartition

English

The (n+1)-th derivative equals the right-composition with the n-th derivative of f.

Русский

$(n+1)$-я производная равна правой композиции с n-й производной f.

LaTeX

$$$\operatorname{iteratedFDeriv}_{\mathbb{k}}(n+1)\ f = (\text{currying})^{−1} \circ \operatorname{iteratedFDeriv}_{\mathbb{k}}(n) (\lambda y.\ fderiv_{\mathbb{k}} f\ y)$$$

Lean4

instance instDecidableEqOrderedFinpartition {n✝} : DecidableEq✝ (@OrderedFinpartition✝ n✝) :=
  instDecidableEqOrderedFinpartition.decEq

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