instMonad

Mathlib.GroupTheory.FreeGroup.Basic

URI: https://scilib.ai/kg/mathlib#FreeGroup.instMonad

English

For any f, f <$> pure x = pure (f x).

Русский

Для любого f выполняется f <$> pure x = pure (f x).

LaTeX

$$$ f <$> (\\text{pure } x) = \\text{pure } (f x) $$$

Lean4

@[to_additive]
instance : Monad FreeGroup.{u} where
  pure {_α} := of
  map {_α _β f} := map f
  bind {_α _β x f} := lift f x

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

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

Разделы

Аффилиация

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