Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-25 01:40 d04f5a55

View on Github →

feat(algebra/pointwise): lemmas about multiplication of finsets (#10455)

Estimated changes

modified theorem finset.coe_mul
added theorem finset.empty_mul
modified theorem finset.mem_mul
modified theorem finset.mul_card_le
modified theorem finset.mul_def
added theorem finset.mul_empty
modified theorem finset.mul_mem_mul
added theorem finset.mul_subset_mul