Mathlib/Algebra/FreeMonoid/Count.lean

Stream: mathlib4

[Kim Morrison]

There is lots of defeq abuse here of FreeAddMonoid α = List α, e.g. in statements like

theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl

Anyone interested in cleaning up?

[Edward van de Meent]

i've looked at this design before, since i wanted to use this for my free probability project... i think this should not be too difficult?

[Edward van de Meent]

In 12 hours, I'll take a look if noone else has

[Edward van de Meent]

is it an idea to have to_additive remove Multiplicative or add Additive automatically (in certain cases?)

[Edward van de Meent]

because right now, we have to write out both docs#FreeMonoid.countP and docs#FreeAddMonoid.countP...

[Edward van de Meent]

just came across docs#List.countP_singleton, which has if p a = true then ... in the rhs where p a : Bool...

[Edward van de Meent]

actually nvm, that seems to be a quirk of pretty printing?
actually the pretty printing is accurate, i just didn't have the right mental model of ite

[Edward van de Meent]

pr at #20156