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 too much because it can't map Multiplicative to .

def FreeMonoid.countP' {α : Type u_1} (p : αProp) [DecidablePred p] (l : FreeMonoid α) :

List.countP lifted to free monoids

Equations
def FreeAddMonoid.countP' {α : Type u_1} (p : αProp) [DecidablePred p] (l : FreeAddMonoid α) :

List.countP lifted to free additive monoids

Equations
theorem FreeMonoid.countP'_one {α : Type u_1} (p : αProp) [DecidablePred p] :
countP' p 1 = 0
theorem FreeAddMonoid.countP'_zero {α : Type u_1} (p : αProp) [DecidablePred p] :
countP' p 0 = 0
theorem FreeMonoid.countP'_mul {α : Type u_1} (p : αProp) [DecidablePred p] (l₁ l₂ : FreeMonoid α) :
countP' p (l₁ * l₂) = countP' p l₁ + countP' p l₂
theorem FreeAddMonoid.countP'_add {α : Type u_1} (p : αProp) [DecidablePred p] (l₁ l₂ : FreeAddMonoid α) :
countP' p (l₁ + l₂) = countP' p l₁ + countP' p l₂

List.countP as a bundled multiplicative monoid homomorphism.

Equations
theorem FreeMonoid.countP_apply {α : Type u_1} (p : αProp) [DecidablePred p] (l : FreeMonoid α) :
(countP p) l = Multiplicative.ofAdd (List.countP (fun (b : α) => decide (p b)) (toList l))
theorem FreeMonoid.countP_of {α : Type u_1} (p : αProp) [DecidablePred p] (x : α) :

List.count as a bundled additive monoid homomorphism.

Equations
theorem FreeMonoid.count_of {α : Type u_1} [DecidableEq α] (x y : α) :
def FreeAddMonoid.countP {α : Type u_1} (p : αProp) [DecidablePred p] :

List.countP as a bundled additive monoid homomorphism.

Equations
theorem FreeAddMonoid.countP_apply {α : Type u_1} (p : αProp) [DecidablePred p] (l : FreeAddMonoid α) :
(countP p) l = List.countP (fun (b : α) => decide (p b)) (toList l)
theorem FreeAddMonoid.countP_of {α : Type u_1} (p : αProp) [DecidablePred p] (x : α) :
(countP p) (of x) = if p x then 1 else 0
def FreeAddMonoid.count {α : Type u_1} [DecidableEq α] (x : α) :

List.count as a bundled additive monoid homomorphism.

Equations
theorem FreeAddMonoid.count_of {α : Type u_1} [DecidableEq α] (x y : α) :
(count x) (of y) = Pi.single x 1 y
theorem FreeAddMonoid.count_apply {α : Type u_1} [DecidableEq α] (x : α) (l : FreeAddMonoid α) :
(count x) l = List.count x (toList l)