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

ink

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

List.countp as a bundled additive monoid homomorphism.

Equations

• One or more equations did not get rendered due to their size.

ink

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

ink

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

ink

def FreeAddMonoid.count {α : Type u_1} [inst : DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ

List.count as a bundled additive monoid homomorphism.

Equations

• FreeAddMonoid.count x = FreeAddMonoid.countp fun x => x = x

ink

theorem FreeAddMonoid.count_of {α : Type u_1} [inst : DecidableEq α] (x : α) (y : α) : ↑(FreeAddMonoid.count x) (FreeAddMonoid.of y) = Pi.single x 1 y

ink

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

ink

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

list.countp as a bundled multiplicative monoid homomorphism.

Equations

• FreeMonoid.countp p = ↑AddMonoidHom.toMultiplicative (FreeAddMonoid.countp p)

ink

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

ink

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

ink

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

ink

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

List.count as a bundled additive monoid homomorphism.

Equations

• FreeMonoid.count x = FreeMonoid.countp fun x => x = x

ink

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

ink

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