Theorems · Theorem

Traversable.foldMap_hom_free

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

Defined in

Mathlib.Control.Fold

Cited by

5 results in Mathlib

Foundations

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

Assumes

TraversableLawfulTraversableMonoid