Theorems · Theorem

Traversable.foldMap_hom

∀ {α β γ : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] [inst_2 : Monoid α]
  [inst_3 : Monoid β] (f : α →* β) (g : γ → α) (x : t γ), f (Traversable.foldMap g x) = Traversable.foldMap (⇑f ∘ g) x

Defined in

Mathlib.Control.Fold

Cited by

2 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

TraversableLawfulTraversableMonoidMonoid