English
FreeGroup is equipped with a lawful monad structure, i.e., the monad laws hold for pure, bind, and map operations.
Русский
Свободная группа образует законную монаду: выполняются все монадные законы для операций pure, bind и map.
LaTeX
$$$$ \\text{LawfulMonad}(\\mathrm{FreeGroup}) $$$$
Lean4
@[to_additive]
instance : LawfulMonad FreeGroup.{u} :=
LawfulMonad.mk' (id_map := fun x =>
FreeGroup.induction_on x (map_one id) (fun x => map_pure id x) (fun x ih => by rw [map_inv, ih]) fun x y ihx ihy =>
by rw [map_mul, ihx, ihy])
(pure_bind := fun x f => pure_bind f x) (bind_assoc := fun x => by
refine FreeGroup.induction_on x ?_ ?_ ?_ ?_ <;> simp +contextual [instMonad]) (bind_pure_comp := fun f x => by
refine FreeGroup.induction_on x ?_ ?_ ?_ ?_ <;> simp +contextual [instMonad])
