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

List.countP as a bundled additive monoid homomorphism.

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.

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.

Instances For
theorem FreeMonoid.countP_of' {α : Type u_1} (p : αProp) [] (x : α) :
↑() () = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
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.

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