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 ℕ.

source
def free_add_monoid.countp {α : Type u_1} (p : α → Prop) [decidable_pred p] :
free_add_monoid α →+ ℕ

list.countp as a bundled additive monoid homomorphism.

Equations
source
theorem free_add_monoid.countp_of {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : α) :
⇑(free_add_monoid.countp p) (free_add_monoid.of x) = ite (p x) 1 0
source
theorem free_add_monoid.countp_apply {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : free_add_monoid α) :
⇑(free_add_monoid.countp p) l = list.countp p l
source
def free_add_monoid.count {α : Type u_1} [decidable_eq α] (x : α) :
free_add_monoid α →+ ℕ

list.count as a bundled additive monoid homomorphism.

Equations
source
theorem free_add_monoid.count_of {α : Type u_1} [decidable_eq α] (x y : α) :
⇑(free_add_monoid.count x) (free_add_monoid.of y) = pi.single x 1 y
source
theorem free_add_monoid.count_apply {α : Type u_1} [decidable_eq α] (x : α) (l : free_add_monoid α) :
⇑(free_add_monoid.count x) l = list.count x l
source
def free_monoid.countp {α : Type u_1} (p : α → Prop) [decidable_pred p] :
free_monoid α →* multiplicative ℕ

list.countp as a bundled multiplicative monoid homomorphism.

Equations
source
theorem free_monoid.countp_of' {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : α) :
⇑(free_monoid.countp p) (free_monoid.of x) = ite (p x) (⇑multiplicative.of_add 1) (⇑multiplicative.of_add 0)
source
theorem free_monoid.countp_of {α : Type u_1} (p : α → Prop) [decidable_pred p] (x : α) :
⇑(free_monoid.countp p) (free_monoid.of x) = ite (p x) (⇑multiplicative.of_add 1) 1
source
theorem free_monoid.countp_apply {α : Type u_1} (p : α → Prop) [decidable_pred p] (l : free_add_monoid α) :
⇑(free_monoid.countp p) l = ⇑multiplicative.of_add (list.countp p l)
source
def free_monoid.count {α : Type u_1} [decidable_eq α] (x : α) :
free_monoid α →* multiplicative ℕ

list.count as a bundled additive monoid homomorphism.

Equations
source
theorem free_monoid.count_apply {α : Type u_1} [decidable_eq α] (x : α) (l : free_add_monoid α) :
⇑(free_monoid.count x) l = ⇑multiplicative.of_add (list.count x l)
source
theorem free_monoid.count_of {α : Type u_1} [decidable_eq α] (x y : α) :
⇑(free_monoid.count x) (free_monoid.of y) = pi.mul_single x (⇑multiplicative.of_add 1) y