Commit 2023-02-01 10:16 e50f014c

View on Github →

feat: Port/Data.Finset.Pointwise (#1911) port of data.finset.pointwise

Estimated changes

added theorem Finset.Nonempty.div
added theorem Finset.Nonempty.mul
added theorem Finset.Nonempty.smul
added theorem Finset.Nonempty.vsub
added theorem Finset.add_mul_subset
added theorem Finset.card_inv
added theorem Finset.card_inv_le
added theorem Finset.card_mul_iff
added theorem Finset.card_mul_le
added theorem Finset.coe_div
added theorem Finset.coe_inv
added theorem Finset.coe_list_prod
added theorem Finset.coe_mul
added theorem Finset.coe_one
added theorem Finset.coe_pow
added theorem Finset.coe_prod
added theorem Finset.coe_smul
added theorem Finset.coe_smul_finset
added theorem Finset.coe_vsub
added theorem Finset.coe_zpow
added theorem Finset.div_card_le
added theorem Finset.div_def
added theorem Finset.div_empty
added theorem Finset.div_eq_empty
added theorem Finset.div_mem_div
added theorem Finset.div_nonempty
added theorem Finset.div_singleton
added theorem Finset.div_subset_div
added theorem Finset.div_subset_iff
added theorem Finset.div_union
added theorem Finset.div_zero_subset
added theorem Finset.empty_div
added theorem Finset.empty_mul
added theorem Finset.empty_pow
added theorem Finset.empty_smul
added theorem Finset.empty_vsub
added theorem Finset.image_div
added theorem Finset.image_div_prod
added theorem Finset.image_inv
added theorem Finset.image_mul
added theorem Finset.image_mul_left'
added theorem Finset.image_mul_left
added theorem Finset.image_mul_right
added theorem Finset.image_one
added theorem Finset.image_smul
added theorem Finset.inv_def
added theorem Finset.inv_empty
added theorem Finset.inv_insert
added theorem Finset.inv_mem_inv
added theorem Finset.inv_singleton
added theorem Finset.inv_subset_inv
added theorem Finset.isUnit_coe
added theorem Finset.isUnit_iff
added theorem Finset.mem_div
added theorem Finset.mem_inv
added theorem Finset.mem_mul
added theorem Finset.mem_one
added theorem Finset.mem_pow
added theorem Finset.mem_smul
added theorem Finset.mem_smul_finset
added theorem Finset.mem_vsub
added theorem Finset.mul_add_subset
added theorem Finset.mul_def
added theorem Finset.mul_empty
added theorem Finset.mul_eq_empty
added theorem Finset.mul_mem_mul
added theorem Finset.mul_nonempty
added theorem Finset.mul_singleton
added theorem Finset.mul_subset_iff
added theorem Finset.mul_subset_mul
added theorem Finset.mul_union
added theorem Finset.mul_zero_subset
added theorem Finset.neg_smul_finset
added theorem Finset.one_mem_div_iff
added theorem Finset.one_mem_one
added theorem Finset.one_nonempty
added theorem Finset.one_subset
added theorem Finset.pow_mem_pow
added theorem Finset.pow_subset_pow
added theorem Finset.preimage_inv
added theorem Finset.singleton_div
added theorem Finset.singleton_mul
added theorem Finset.singleton_one
added theorem Finset.singleton_smul
added theorem Finset.singleton_vsub
added theorem Finset.smul_card_le
added theorem Finset.smul_def
added theorem Finset.smul_empty
added theorem Finset.smul_eq_empty
added theorem Finset.smul_finset_def
added theorem Finset.smul_finset_neg
added theorem Finset.smul_mem_smul
added theorem Finset.smul_singleton
added theorem Finset.smul_subset_iff
added theorem Finset.smul_union
added theorem Finset.smul_univ₀
added theorem Finset.subset_div
added theorem Finset.subset_mul
added theorem Finset.subset_mul_left
added theorem Finset.subset_smul
added theorem Finset.subset_vsub
added theorem Finset.union_div
added theorem Finset.union_mul
added theorem Finset.union_smul
added theorem Finset.union_vsub
added theorem Finset.univ_mul_univ
added theorem Finset.univ_pow
added theorem Finset.vsub_card_le
added theorem Finset.vsub_def
added theorem Finset.vsub_empty
added theorem Finset.vsub_eq_empty
added theorem Finset.vsub_mem_vsub
added theorem Finset.vsub_nonempty
added theorem Finset.vsub_singleton
added theorem Finset.vsub_subset_iff
added theorem Finset.vsub_union
added theorem Finset.zero_div_subset
added theorem Finset.zero_mul_subset