Theorems · Theorem

Traversable.foldMap_map

∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] [inst_2 : Monoid γ] (f : α → β)
  (g : β → γ) (xs : t α), Traversable.foldMap g (f <$> xs) = Traversable.foldMap (g ∘ f) xs

Defined in

Mathlib.Control.Fold

Cited by

5 results in Mathlib

Foundations

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

Assumes

TraversableLawfulTraversableMonoid