Commit 2022-07-29 12:50 0fc357f5

View on Github →

feat(data/finset/pointwise): Singleton arithmetic (#15435) Lemmas about pointwise operations with a singleton. Also make s explicit in finset.card_inv.

Estimated changes

Modified src/data/finset/n_ary.lean

added theorem finset.card_image₂_singleton_left

added theorem finset.card_image₂_singleton_right

added theorem finset.card_le_card_image₂_left

added theorem finset.card_le_card_image₂_right

added theorem finset.image₂_inter_singleton

added theorem finset.image₂_singleton_inter

Modified src/data/finset/pointwise.lean

added theorem finset.card_le_card_mul_left

added theorem finset.card_le_card_mul_right

added theorem finset.card_mul_singleton

added theorem finset.card_singleton_mul

modified theorem finset.coe_inv

added theorem finset.inter_mul_singleton

modified theorem finset.mul_singleton

modified theorem finset.pairwise_disjoint_smul_iff

modified theorem finset.singleton_mul

added theorem finset.singleton_mul_inter

modified theorem finset.singleton_smul

modified theorem finset.singleton_vsub

modified theorem finset.smul_singleton