Commit 2025-03-30 23:38 f36aa847

View on Github →

chore(Algebra/Group/Pointwise/{Fin}set/Basic): split files (#23429) This PR splits the files on pointwise operations on sets, creating new files for the scalar multiplication etc. operations. This addresses an instance of the long file linter, while keeping the directory structure analogous.

Estimated changes

deleted theorem Finset.Nonempty.smul
deleted theorem Finset.Nonempty.vsub
deleted theorem Finset.card_smul_le
deleted theorem Finset.coe_smul
deleted theorem Finset.coe_smul_finset
deleted theorem Finset.coe_vsub
deleted theorem Finset.empty_smul
deleted theorem Finset.empty_vsub
deleted theorem Finset.image_smul
deleted theorem Finset.image_smul_comm
deleted theorem Finset.image_smul_product
deleted theorem Finset.image_vsub_product
deleted theorem Finset.inter_smul_subset
deleted theorem Finset.inter_vsub_subset
deleted theorem Finset.mem_smul
deleted theorem Finset.mem_smul_finset
deleted theorem Finset.mem_vsub
deleted theorem Finset.singleton_smul
deleted theorem Finset.singleton_vsub
deleted theorem Finset.smul_def
deleted theorem Finset.smul_empty
deleted theorem Finset.smul_eq_empty
deleted theorem Finset.smul_finset_def
deleted theorem Finset.smul_finset_empty
deleted theorem Finset.smul_finset_insert
deleted theorem Finset.smul_finset_union
deleted theorem Finset.smul_inter_subset
deleted theorem Finset.smul_mem_smul
deleted theorem Finset.smul_nonempty_iff
deleted theorem Finset.smul_singleton
deleted theorem Finset.smul_subset_iff
deleted theorem Finset.smul_subset_smul
deleted theorem Finset.smul_union
deleted theorem Finset.subset_smul
deleted theorem Finset.subset_vsub
deleted theorem Finset.union_smul
deleted theorem Finset.union_vsub
deleted theorem Finset.vsub_card_le
deleted theorem Finset.vsub_def
deleted theorem Finset.vsub_empty
deleted theorem Finset.vsub_eq_empty
deleted theorem Finset.vsub_inter_subset
deleted theorem Finset.vsub_mem_vsub
deleted theorem Finset.vsub_nonempty
deleted theorem Finset.vsub_singleton
deleted theorem Finset.vsub_subset_iff
deleted theorem Finset.vsub_subset_vsub
deleted theorem Finset.vsub_union
deleted theorem Set.Finite.toFinset_smul
deleted theorem Set.Finite.toFinset_vsub
deleted theorem Set.toFinset_smul
deleted theorem Set.toFinset_smul_set
deleted theorem Set.toFinset_vsub
added theorem Finset.Nonempty.smul
added theorem Finset.Nonempty.vsub
added theorem Finset.card_smul_le
added theorem Finset.coe_smul
added theorem Finset.coe_smul_finset
added theorem Finset.coe_vsub
added theorem Finset.empty_smul
added theorem Finset.empty_vsub
added theorem Finset.image_smul
added theorem Finset.image_smul_comm
added theorem Finset.mem_smul
added theorem Finset.mem_smul_finset
added theorem Finset.mem_vsub
added theorem Finset.singleton_smul
added theorem Finset.singleton_vsub
added theorem Finset.smul_def
added theorem Finset.smul_empty
added theorem Finset.smul_eq_empty
added theorem Finset.smul_finset_def
added theorem Finset.smul_mem_smul
added theorem Finset.smul_singleton
added theorem Finset.smul_subset_iff
added theorem Finset.smul_union
added theorem Finset.subset_smul
added theorem Finset.subset_vsub
added theorem Finset.union_smul
added theorem Finset.union_vsub
added theorem Finset.vsub_card_le
added theorem Finset.vsub_def
added theorem Finset.vsub_empty
added theorem Finset.vsub_eq_empty
added theorem Finset.vsub_mem_vsub
added theorem Finset.vsub_nonempty
added theorem Finset.vsub_singleton
added theorem Finset.vsub_subset_iff
added theorem Finset.vsub_union
added theorem Set.toFinset_smul
added theorem Set.toFinset_smul_set
added theorem Set.toFinset_vsub
deleted theorem Set.Nonempty.of_smul_left
deleted theorem Set.Nonempty.of_vsub_left
deleted theorem Set.Nonempty.smul
deleted theorem Set.Nonempty.smul_set
deleted theorem Set.Nonempty.vsub
deleted theorem Set.empty_smul
deleted theorem Set.empty_vsub
deleted theorem Set.image2_smul
deleted theorem Set.image2_vsub
deleted theorem Set.image_smul
deleted theorem Set.image_smul_comm
deleted theorem Set.image_smul_prod
deleted theorem Set.image_vsub_prod
deleted theorem Set.inter_smul_subset
deleted theorem Set.inter_vsub_subset
deleted theorem Set.mem_smul
deleted theorem Set.mem_smul_set
deleted theorem Set.mem_vsub
deleted theorem Set.range_smul
deleted theorem Set.range_smul_range
deleted theorem Set.singleton_smul
deleted theorem Set.singleton_vsub
deleted theorem Set.smul_empty
deleted theorem Set.smul_eq_empty
deleted theorem Set.smul_inter_subset
deleted theorem Set.smul_mem_smul
deleted theorem Set.smul_mem_smul_set
deleted theorem Set.smul_nonempty
deleted theorem Set.smul_set_empty
deleted theorem Set.smul_set_eq_empty
deleted theorem Set.smul_set_insert
deleted theorem Set.smul_set_inter_subset
deleted theorem Set.smul_set_mono
deleted theorem Set.smul_set_nonempty
deleted theorem Set.smul_set_range
deleted theorem Set.smul_set_singleton
deleted theorem Set.smul_set_subset_iff
deleted theorem Set.smul_set_subset_smul
deleted theorem Set.smul_set_union
deleted theorem Set.smul_set_univ_pi
deleted theorem Set.smul_singleton
deleted theorem Set.smul_subset_iff
deleted theorem Set.smul_subset_smul
deleted theorem Set.smul_subset_smul_left
deleted theorem Set.smul_union
deleted theorem Set.union_smul
deleted theorem Set.union_vsub
deleted theorem Set.vsub_empty
deleted theorem Set.vsub_eq_empty
deleted theorem Set.vsub_inter_subset
deleted theorem Set.vsub_mem_vsub
deleted theorem Set.vsub_nonempty
deleted theorem Set.vsub_self_mono
deleted theorem Set.vsub_singleton
deleted theorem Set.vsub_subset_iff
deleted theorem Set.vsub_subset_vsub
deleted theorem Set.vsub_subset_vsub_left
deleted theorem Set.vsub_union
added theorem Set.Nonempty.smul
added theorem Set.Nonempty.smul_set
added theorem Set.Nonempty.vsub
added theorem Set.empty_smul
added theorem Set.empty_vsub
added theorem Set.image2_smul
added theorem Set.image2_vsub
added theorem Set.image_smul
added theorem Set.image_smul_comm
added theorem Set.image_smul_prod
added theorem Set.image_vsub_prod
added theorem Set.inter_smul_subset
added theorem Set.inter_vsub_subset
added theorem Set.mem_smul
added theorem Set.mem_smul_set
added theorem Set.mem_vsub
added theorem Set.range_smul
added theorem Set.range_smul_range
added theorem Set.singleton_smul
added theorem Set.singleton_vsub
added theorem Set.smul_empty
added theorem Set.smul_eq_empty
added theorem Set.smul_inter_subset
added theorem Set.smul_mem_smul
added theorem Set.smul_mem_smul_set
added theorem Set.smul_nonempty
added theorem Set.smul_set_empty
added theorem Set.smul_set_eq_empty
added theorem Set.smul_set_insert
added theorem Set.smul_set_mono
added theorem Set.smul_set_nonempty
added theorem Set.smul_set_range
added theorem Set.smul_set_singleton
added theorem Set.smul_set_union
added theorem Set.smul_set_univ_pi
added theorem Set.smul_singleton
added theorem Set.smul_subset_iff
added theorem Set.smul_subset_smul
added theorem Set.smul_union
added theorem Set.union_smul
added theorem Set.union_vsub
added theorem Set.vsub_empty
added theorem Set.vsub_eq_empty
added theorem Set.vsub_inter_subset
added theorem Set.vsub_mem_vsub
added theorem Set.vsub_nonempty
added theorem Set.vsub_self_mono
added theorem Set.vsub_singleton
added theorem Set.vsub_subset_iff
added theorem Set.vsub_subset_vsub
added theorem Set.vsub_union