Theorems · Theorem

Traversable.foldlm_map

∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {m : Type u → Type u}
  [inst_2 : Monad m] [LawfulMonad m] (g : β → γ) (f : α → γ → m α) (a : α) (l : t β),
  Traversable.foldlm f a (g <$> l) = Traversable.foldlm (fun x y => f x (g y)) a l

Defined in

Mathlib.Control.Fold

Cited by

0 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Quot.sound

Assumes

TraversableLawfulTraversableMonadLawfulMonad