Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-02 21:37 ca1551c2

View on Github →

feat(data/finset/n_ary): Binary image of finsets (#13718) Define finset.image₂, the binary map of finsets. Golf data.finset.pointwise using it.

Estimated changes

added theorem finset.card_image₂
added theorem finset.coe_image₂
added theorem finset.image_image₂
added def finset.image₂
added theorem finset.image₂_assoc
added theorem finset.image₂_comm
added theorem finset.image₂_congr'
added theorem finset.image₂_congr
added theorem finset.image₂_left
added theorem finset.image₂_right
added theorem finset.image₂_subset
added theorem finset.image₂_swap
added theorem finset.mem_image₂
added theorem finset.subset_image₂
modified theorem finset.coe_div
modified theorem finset.coe_mul
modified theorem finset.coe_vsub
modified theorem finset.div_card_le
modified theorem finset.div_empty
modified theorem finset.div_mem_div
modified theorem finset.div_singleton
modified theorem finset.div_subset_div
modified theorem finset.empty_div
modified theorem finset.empty_mul
modified theorem finset.empty_smul
modified theorem finset.empty_vsub
modified theorem finset.image_vsub_product
modified theorem finset.mem_div
modified theorem finset.mem_mul
modified theorem finset.mem_smul
modified theorem finset.mem_vsub
modified theorem finset.mul_card_le
modified theorem finset.mul_empty
modified theorem finset.mul_mem_mul
modified theorem finset.mul_singleton
modified theorem finset.mul_subset_mul
added theorem finset.nonempty.div
added theorem finset.nonempty.mul
modified theorem finset.nonempty.smul
modified theorem finset.nonempty.vsub
modified theorem finset.singleton_div
modified theorem finset.singleton_mul
modified theorem finset.singleton_smul
modified theorem finset.smul_card_le
modified theorem finset.smul_empty
modified theorem finset.smul_mem_smul
modified theorem finset.smul_nonempty_iff
modified theorem finset.smul_singleton
modified theorem finset.smul_subset_smul
modified theorem finset.subset_div
modified theorem finset.subset_mul
modified theorem finset.subset_smul
modified theorem finset.subset_vsub
modified theorem finset.vsub_card_le
modified theorem finset.vsub_def
modified theorem finset.vsub_empty
modified theorem finset.vsub_mem_vsub
modified theorem finset.vsub_nonempty_iff
modified theorem finset.vsub_subset_vsub