mathlib
eb3d6001 - feat(data/{list,multiset}): add `can_lift` instances (#9262)

Commit
4 years ago
feat(data/{list,multiset}): add `can_lift` instances (#9262) * add `can_lift` instances for `set`, `list`, `multiset`, and `finset`; * use them in `submonoid.{list,multiset}_prod_mem`; * more `to_additive` attrs in `group_theory.submonoid.membership`.
Author
Parents
Loading