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 ℕ
.
theorem
FreeMonoid.countP'_mul
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(l₁ l₂ : FreeMonoid α)
:
theorem
FreeAddMonoid.countP'_add
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(l₁ l₂ : FreeAddMonoid α)
:
List.countP
as a bundled multiplicative monoid homomorphism.
Equations
Instances For
theorem
FreeMonoid.countP_apply
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(l : FreeMonoid α)
:
List.countP
as a bundled additive monoid homomorphism.
Equations
- FreeAddMonoid.countP p = { toFun := FreeAddMonoid.countP' p, map_zero' := ⋯, map_add' := ⋯ }
Instances For
theorem
FreeAddMonoid.countP_apply
{α : Type u_1}
(p : α → Prop)
[DecidablePred p]
(l : FreeAddMonoid α)
:
List.count
as a bundled additive monoid homomorphism.