mathlib
68d9b42b - feat(data/list/count): add lemma `list.count_singleton'` (#10880)

Commit
4 years ago
feat(data/list/count): add lemma `list.count_singleton'` (#10880) A generalisation of `count_singleton`: `count a [b] = ite (a = b) 1 0`
Parents
Loading