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) [DecidablePred p] : FreeAddMonoid α →+ ℕ

List.countP as a bundled additive monoid homomorphism.

theorem FreeAddMonoid.countP_of {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : ↑(FreeAddMonoid.countP p) (FreeAddMonoid.of x) = if p x = (true = true) then 1 else 0

theorem FreeAddMonoid.countP_apply {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : FreeAddMonoid α) : ↑(FreeAddMonoid.countP p) l = List.countP (fun b => decide (p b)) l

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 : α) : ↑(FreeAddMonoid.count x) (FreeAddMonoid.of y) = Pi.single x 1 y

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

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

List.countP as a bundled multiplicative monoid homomorphism.

theorem FreeMonoid.countP_of' {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : ↑(FreeMonoid.countP p) (FreeMonoid.of x) = if p x then ↑Multiplicative.ofAdd 1 else ↑Multiplicative.ofAdd 0

theorem FreeMonoid.countP_of {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : ↑(FreeMonoid.countP p) (FreeMonoid.of x) = if p x then ↑Multiplicative.ofAdd 1 else 1

theorem FreeMonoid.countP_apply {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : FreeAddMonoid α) : ↑(FreeMonoid.countP p) l = ↑Multiplicative.ofAdd (List.countP (fun b => decide (p b)) l)

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 α) : ↑(FreeMonoid.count x) l = ↑Multiplicative.ofAdd (List.count x l)

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