Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 11:08 86055c5d

View on Github →

split(data/{finset,set}/pointwise): Split off algebra.pointwise (#12831) Split algebra.pointwise into

  • data.set.pointwise: Pointwise operations on set
  • data.finset.pointwise: Pointwise operations on finset I'm crediting
  • The same people for data.set.pointwise
  • Floris for #3541

Estimated changes

added theorem finset.coe_mul
added theorem finset.coe_one
added theorem finset.coe_pow
added theorem finset.empty_mul
added theorem finset.image_mul_left'
added theorem finset.image_mul_left
added theorem finset.image_mul_prod
added theorem finset.image_mul_right
added theorem finset.image_one
added theorem finset.mem_mul
added theorem finset.mem_one
added theorem finset.mul_card_le
added theorem finset.mul_def
added theorem finset.mul_empty
added theorem finset.mul_mem_mul
added theorem finset.mul_singleton
added theorem finset.mul_subset_mul
added theorem finset.mul_zero_subset
added theorem finset.one_mem_one
added theorem finset.one_nonempty
added theorem finset.one_subset
added theorem finset.singleton_mul
added theorem finset.singleton_one
added theorem finset.subset_mul
added theorem finset.zero_mul_subset
deleted theorem finset.coe_mul
deleted theorem finset.coe_one
deleted theorem finset.coe_pow
deleted theorem finset.empty_mul
deleted theorem finset.image_mul_left'
deleted theorem finset.image_mul_left
deleted theorem finset.image_mul_prod
deleted theorem finset.image_mul_right'
deleted theorem finset.image_mul_right
deleted theorem finset.image_one
deleted theorem finset.mem_mul
deleted theorem finset.mem_one
deleted theorem finset.mul_card_le
deleted theorem finset.mul_def
deleted theorem finset.mul_empty
deleted theorem finset.mul_mem_mul
deleted theorem finset.mul_nonempty_iff
deleted theorem finset.mul_singleton
deleted theorem finset.mul_subset_mul
deleted theorem finset.mul_zero_subset
deleted theorem finset.nonempty.mul_zero
deleted theorem finset.nonempty.zero_mul
deleted theorem finset.one_mem_one
deleted theorem finset.one_nonempty
deleted theorem finset.one_subset
deleted theorem finset.singleton_mul
deleted theorem finset.singleton_one
deleted theorem finset.singleton_zero_mul
deleted theorem finset.subset_mul
deleted theorem finset.zero_mul_subset