instLawfulMonad — Mathlib

English

FreeSemigroup is endowed with a lawful monad structure: the monad laws (pure_bind, bind_assoc, id_map) hold.

Русский

У FreeSemigroup есть законное образование монад: законы монад (pure_bind, bind_assoc, id_map) выполняются.

LaTeX

$$$\text{LawfulMonad}(\text{FreeSemigroup})$$$

Lean4

@[to_additive]
instance instLawfulMonad : LawfulMonad FreeSemigroup.{u} :=
  LawfulMonad.mk' (pure_bind := fun _ _ ↦ rfl) (bind_assoc := fun x g f ↦
    recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by rw [mul_bind, mul_bind, mul_bind, ih1, ih2]) (id_map := fun x ↦
    recOnPure x (fun _ ↦ rfl) fun x y ih1 ih2 ↦ by rw [map_mul', ih1, ih2])

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