Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-22 12:35 d5861954

View on Github →

feat(data/finset/pointwise): Missing operations (#12865) Define -s, s⁻¹, s - t, s / t, s +ᵥ t, s • t, s -ᵥ t, a • s, a +ᵥ s for s, t finsets, a scalar. Provide a bare API following what is already there for s + t, s * t.

Estimated changes

added theorem finset.card_inv
added theorem finset.card_inv_le
added theorem finset.coe_div
added theorem finset.coe_inv
modified theorem finset.coe_pow
added theorem finset.coe_smul
added theorem finset.coe_smul_finset
added theorem finset.coe_vsub
added theorem finset.coe_zpow'
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_mem_div
added theorem finset.div_singleton
added theorem finset.div_subset_div
added theorem finset.div_zero_subset
added theorem finset.empty_div
added theorem finset.empty_smul
added theorem finset.empty_vsub
added theorem finset.image_div_prod
added theorem finset.image_inv
added theorem finset.image_smul
added theorem finset.inv_def
added theorem finset.inv_empty
added theorem finset.inv_mem_inv
added theorem finset.inv_singleton
added theorem finset.inv_subset_inv
added theorem finset.mem_div
added theorem finset.mem_inv
added theorem finset.mem_smul
added theorem finset.mem_smul_finset
added theorem finset.mem_vsub
modified theorem finset.mul_card_le
added theorem finset.nonempty.smul
added theorem finset.nonempty.vsub
added theorem finset.preimage_inv
added theorem finset.singleton_div
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_finset_def
added theorem finset.smul_mem_smul
added theorem finset.smul_singleton
added theorem finset.subset_div
added theorem finset.subset_smul
added theorem finset.subset_vsub
added theorem finset.vsub_card_le
added theorem finset.vsub_def
added theorem finset.vsub_empty
added theorem finset.vsub_mem_vsub
added theorem finset.vsub_singleton
added theorem finset.zero_div_subset