# 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) [] :

List.countP as a bundled additive monoid homomorphism.

Equations
• = { toZeroHom := { toFun := List.countP fun (b : α) => decide (p b), map_zero' := }, map_add' := }
Instances For
theorem FreeAddMonoid.countP_of {α : Type u_1} (p : αProp) [] (x : α) :
= if p x = () then 1 else 0
theorem FreeAddMonoid.countP_apply {α : Type u_1} (p : αProp) [] (l : ) :
l = List.countP (fun (b : α) => decide (p b)) l
def FreeAddMonoid.count {α : Type u_1} [] (x : α) :

List.count as a bundled additive monoid homomorphism.

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

List.countP as a bundled multiplicative monoid homomorphism.

Equations
Instances For
theorem FreeMonoid.countP_of' {α : Type u_1} (p : αProp) [] (x : α) :
theorem FreeMonoid.countP_of {α : Type u_1} (p : αProp) [] (x : α) :
() = if p x then Multiplicative.ofAdd 1 else 1
theorem FreeMonoid.countP_apply {α : Type u_1} (p : αProp) [] (l : ) :
l = Multiplicative.ofAdd (List.countP (fun (b : α) => decide (p b)) l)
def FreeMonoid.count {α : Type u_1} [] (x : α) :

List.count as a bundled additive monoid homomorphism.

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