# mathlib3documentation

algebra.free_monoid.count

# list.count as a bundled homomorphism #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define free_monoid.countp, free_monoid.count, free_add_monoid.countp, and free_add_monoid.count. These are list.countp and list.count bundled as multiplicative and additive homomorphisms from free_monoid and free_add_monoid.

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

def free_add_monoid.countp {α : Type u_1} (p : α Prop)  :

list.countp as a bundled additive monoid homomorphism.

Equations
theorem free_add_monoid.countp_of {α : Type u_1} (p : α Prop) (x : α) :
= ite (p x) 1 0
theorem free_add_monoid.countp_apply {α : Type u_1} (p : α Prop) (l : free_add_monoid α) :
= l
def free_add_monoid.count {α : Type u_1} [decidable_eq α] (x : α) :

list.count as a bundled additive monoid homomorphism.

Equations
theorem free_add_monoid.count_of {α : Type u_1} [decidable_eq α] (x y : α) :
= 1 y
theorem free_add_monoid.count_apply {α : Type u_1} [decidable_eq α] (x : α) (l : free_add_monoid α) :
= l
def free_monoid.countp {α : Type u_1} (p : α Prop)  :

list.countp as a bundled multiplicative monoid homomorphism.

Equations
theorem free_monoid.countp_of' {α : Type u_1} (p : α Prop) (x : α) :
= ite (p x)
theorem free_monoid.countp_of {α : Type u_1} (p : α Prop) (x : α) :
= ite (p x) 1
theorem free_monoid.countp_apply {α : Type u_1} (p : α Prop) (l : free_add_monoid α) :
def free_monoid.count {α : Type u_1} [decidable_eq α] (x : α) :

list.count as a bundled additive monoid homomorphism.

Equations
theorem free_monoid.count_apply {α : Type u_1} [decidable_eq α] (x : α) (l : free_add_monoid α) :
l =
theorem free_monoid.count_of {α : Type u_1} [decidable_eq α] (x y : α) :
=