mvfunctorM

Mathlib.Data.PFunctor.Multivariate.M

URI: https://scilib.ai/kg/mathlib#MvPFunctor.mvfunctorM

English

There is a natural MvFunctor structure on MvPFunctor M, providing a functorial action on the M-type.

Русский

Существует естественная структура MV-функтор на MvPFunctor M, задающая действие функторности на M‑тип.

LaTeX

$$$\\text{mvfunctorM}: \\text{MvFunctor } P.M$$$

Lean4

instance mvfunctorM : MvFunctor P.M := by delta M; infer_instance

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru