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

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

List.countP lifted to free additive monoids

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₂

def FreeMonoid.countP {α : Type u_1} (p : α → Prop) [DecidablePred p] : FreeMonoid α →* Multiplicative ℕ

List.countP as a bundled multiplicative monoid homomorphism.

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 : α) : (countP p) (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

def FreeMonoid.count {α : Type u_1} [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ

List.count as a bundled additive monoid homomorphism.

theorem FreeMonoid.count_apply {α : Type u_1} [DecidableEq α] (x : α) (l : FreeAddMonoid α) : (count x) l = Multiplicative.ofAdd (List.count x (FreeAddMonoid.toList l))

theorem FreeMonoid.count_of {α : Type u_1} [DecidableEq α] (x y : α) : (count x) (of y) = Pi.mulSingle x (Multiplicative.ofAdd 1) y

def FreeAddMonoid.countP {α : Type u_1} (p : α → Prop) [DecidablePred p] : FreeAddMonoid α →+ ℕ

List.countP as a bundled additive monoid homomorphism.

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 : α) : FreeAddMonoid α →+ ℕ

List.count as a bundled additive monoid homomorphism.

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)