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 ℕ
.
List.countP
as a bundled additive monoid homomorphism.
Instances For
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
List.count
as a bundled additive monoid homomorphism.
Instances For
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
List.countP
as a bundled multiplicative monoid homomorphism.
Instances For
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)
List.count
as a bundled additive monoid homomorphism.
Instances For
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