Theorems · Theorem · group theory

FreeSemigroup.lift_mk_eq_foldl

∀ {α : Type u} {β : Type v} [inst : Semigroup β] {f : α → β} {x : α} {xs : List α},
  (FreeSemigroup.lift f) { head := x, tail := xs } = List.foldl (fun x1 x2 => x1 * f x2) (f x) xs

Defined in

Mathlib.Algebra.Free

Cited by

0 results in Mathlib

Foundations

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

Assumes

Semigroup