# Documentation

Mathlib.Algebra.FreeMonoid.Count

# List.count as a bundled homomorphism #

In this file we define FreeMonoid.countp, FreeMonoid.count, FreeAddMonoid.countp, and FreeAddMonoid.count. These are List.countp and List.count bundled as multiplicative and additive homomorphisms from FreeMonoid and FreeAddMonoid.

We do not use to_additive because it can't map Multiplicative ℕ to ℕ.

def FreeAddMonoid.countp {α : Type u_1} (p : αProp) [inst : ] :

List.countp as a bundled additive monoid homomorphism.

Equations
• One or more equations did not get rendered due to their size.
theorem FreeAddMonoid.countp_of {α : Type u_1} (p : αProp) [inst : ] (x : α) :
↑() () = if p x = () then 1 else 0
theorem FreeAddMonoid.countp_apply {α : Type u_1} (p : αProp) [inst : ] (l : ) :
↑() l = List.countp (fun b => decide (p b)) l
def FreeAddMonoid.count {α : Type u_1} [inst : ] (x : α) :

List.count as a bundled additive monoid homomorphism.

Equations
theorem FreeAddMonoid.count_of {α : Type u_1} [inst : ] (x : α) (y : α) :
↑() () = Pi.single x 1 y
theorem FreeAddMonoid.count_apply {α : Type u_1} [inst : ] (x : α) (l : ) :
↑() l =
def FreeMonoid.countp {α : Type u_1} (p : αProp) [inst : ] :

list.countp as a bundled multiplicative monoid homomorphism.

Equations
theorem FreeMonoid.countp_of' {α : Type u_1} (p : αProp) [inst : ] (x : α) :
↑() () = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
theorem FreeMonoid.countp_of {α : Type u_1} (p : αProp) [inst : ] (x : α) :
↑() () = if p x then Multiplicative.ofAdd 1 else 1
theorem FreeMonoid.countp_apply {α : Type u_1} (p : αProp) [inst : ] (l : ) :
↑() l = Multiplicative.ofAdd (List.countp (fun b => decide (p b)) l)
def FreeMonoid.count {α : Type u_1} [inst : ] (x : α) :

List.count as a bundled additive monoid homomorphism.

Equations
theorem FreeMonoid.count_apply {α : Type u_1} [inst : ] (x : α) (l : ) :