Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-22 12:11 eb3d6001

View on Github →

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.

Estimated changes

deleted theorem add_submonoid.nsmul_mem
modified theorem submonoid.coe_finset_prod
modified theorem submonoid.coe_list_prod
modified theorem submonoid.coe_multiset_prod
modified theorem submonoid.coe_pow
modified theorem submonoid.list_prod_mem
modified theorem submonoid.multiset_prod_mem
modified theorem submonoid.pow_mem