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

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

List.countp as a bundled additive monoid homomorphism.

Equations
  • One or more equations did not get rendered due to their size.
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
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
def FreeAddMonoid.count {α : Type u_1} [inst : DecidableEq α] (x : α) :

List.count as a bundled additive monoid homomorphism.

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

list.countp as a bundled multiplicative monoid homomorphism.

Equations
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
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
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)
def FreeMonoid.count {α : Type u_1} [inst : DecidableEq α] (x : α) :

List.count as a bundled additive monoid homomorphism.

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