Commit 2024-10-22 14:15 660d68a7

View on Github →

refactor(Group/Pointwise/Finset): state mul_singleton/singleton_mul using • (#18068) This is much more useful in practice than the image spelling. Move the smul/vadd sections higher to allow for that spelling. From LeanCamCombi

Estimated changes

modified theorem Finset.Nonempty.smul
modified theorem Finset.Nonempty.smul_finset
modified theorem Finset.biUnion_smul_finset
modified theorem Finset.coe_smul
modified theorem Finset.coe_smul_finset
modified theorem Finset.empty_smul
modified theorem Finset.image_smul
modified theorem Finset.image_smul_product
modified theorem Finset.inter_smul_subset
modified theorem Finset.mem_smul
modified theorem Finset.mem_smul_finset
modified theorem Finset.mul_singleton
modified theorem Finset.singleton_mul
modified theorem Finset.singleton_smul
modified theorem Finset.smul_card_le
modified theorem Finset.smul_def
modified theorem Finset.smul_empty
modified theorem Finset.smul_eq_empty
modified theorem Finset.smul_finset_card_le
modified theorem Finset.smul_finset_def
modified theorem Finset.smul_finset_empty
modified theorem Finset.smul_finset_eq_empty
modified theorem Finset.smul_finset_nonempty
modified theorem Finset.smul_finset_union
modified theorem Finset.smul_inter_subset
modified theorem Finset.smul_mem_smul
modified theorem Finset.smul_mem_smul_finset
modified theorem Finset.smul_nonempty_iff
modified theorem Finset.smul_singleton
modified theorem Finset.smul_subset_iff
modified theorem Finset.smul_subset_smul
modified theorem Finset.smul_union
modified theorem Finset.subset_smul
modified theorem Finset.union_smul