mathlib
aaf7dc2c - chore(data/multiset/basic): rename theorems, mark as `simp` (#15883)

Commit
3 years ago
chore(data/multiset/basic): rename theorems, mark as `simp` (#15883) This PR does the following: - rename `coe_nil_eq_zero` to `coe_nil`. - rename `singleton_eq_cons` to `cons_zero`, flip direction, mark `simp` (we prefer `{a}` over `a ::ₘ 0`). - add lemmas `coe_singleton` and `singleton_eq_cons_iff`. - ditch `singleton_coe` in favor of `cons_zero` and `coe_singleton`. - mark `singleton_add`, `singleton_inj`, `nodup_singleton` as `simp`. - unmark `count_singleton_self` as `simp`, since it can now be solved automatically via `count_eq_one_of_mem`.
Author
Parents
Loading