Commit 2022-05-21 11:38 f04684f4

chore(data/set/pointwise): Move into the set namespace (#14281) A bunch of lemmas about scalar multiplications of sets were dumped in root namespace for some reason. The lemmas moved to set.* are:

• zero_smul_set
• zero_smul_subset
• subsingleton_zero_smul_set
• zero_mem_smul_set
• zero_mem_smul_iff
• zero_mem_smul_set_iff
• smul_add_set
• smul_mem_smul_set_iff
• mem_smul_set_iff_inv_smul_mem
• mem_inv_smul_set_iff
• preimage_smul
• preimage_smul_inv
• set_smul_subset_set_smul_iff
• set_smul_subset_iff
• subset_set_smul_iff
• smul_mem_smul_set_iff₀
• mem_smul_set_iff_inv_smul_mem₀
• mem_inv_smul_set_iff₀
• preimage_smul₀
• preimage_smul_inv₀
• set_smul_subset_set_smul_iff₀
• set_smul_subset_iff₀
• subset_set_smul_iff₀
• smul_univ₀
• smul_set_univ₀