drop — Mathlib

English

Split polynomial functor to obtain an n-ary functor from an n+1-ary functor by replacing B a with its drop.

Русский

Разделение полиномиального функторa: из n+1-арного функторa получаем n-арный, заменив B a на (B a).drop.

LaTeX

$$$\\text{drop} : \\text{MvPFunctor } n\\;\\text{where } A := P.A,\\ B\\ a := (P.B\\ a).\\text{drop}$$$

Lean4

/-- Split polynomial functor, get an n-ary functor
from an `n+1`-ary functor -/
def drop : MvPFunctor n where
  A := P.A
  B a := (P.B a).drop

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