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]
:
FreeAddMonoid α →+ ℕ
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
List.count
as a bundled additive monoid homomorphism.
Equations
- FreeAddMonoid.count x = FreeAddMonoid.countp fun x => x = x
theorem
FreeAddMonoid.count_of
{α : Type u_1}
[inst : DecidableEq α]
(x : α)
(y : α)
:
↑(FreeAddMonoid.count x) (FreeAddMonoid.of y) = Pi.single x 1 y
theorem
FreeAddMonoid.count_apply
{α : Type u_1}
[inst : DecidableEq α]
(x : α)
(l : FreeAddMonoid α)
:
↑(FreeAddMonoid.count x) l = List.count x l
list.countp
as a bundled multiplicative monoid homomorphism.
Equations
- FreeMonoid.countp p = ↑AddMonoidHom.toMultiplicative (FreeAddMonoid.countp p)
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)
List.count
as a bundled additive monoid homomorphism.
Equations
- FreeMonoid.count x = FreeMonoid.countp fun x => x = x
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