mathlib3 documentation

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

list.countp as a bundled additive monoid homomorphism.

Equations
theorem free_add_monoid.countp_of {α : Type u_1} (p : α Prop) [decidable_pred p] (x : α) :
def free_add_monoid.count {α : Type u_1} [decidable_eq α] (x : α) :

list.count as a bundled additive monoid homomorphism.

Equations
def free_monoid.countp {α : Type u_1} (p : α Prop) [decidable_pred p] :

list.countp as a bundled multiplicative monoid homomorphism.

Equations
theorem free_monoid.countp_of {α : Type u_1} (p : α Prop) [decidable_pred p] (x : α) :

list.count as a bundled additive monoid homomorphism.

Equations