mathlib

f04684f4 - chore(data/set/pointwise): Move into the `set` namespace (#14281)

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₀`