Commit 2022-12-03 13:15 9114ddff

View on Github →

chore(data/set/pointwise/basic): split (#17768) Split off new files data/set/pointwise/smul and data/set/pointwise/finite from data/set/pointwise/basic, reducing imports of the basic file.

Estimated changes

Modified archive/100-theorems-list/82_cubing_a_cube.lean

Modified src/algebra/add_torsor.lean

Modified src/algebra/bounds.lean

Modified src/algebra/module/linear_map.lean

Modified src/algebra/module/pointwise_pi.lean

Modified src/algebra/order/interval.lean

Modified src/algebra/order/pointwise.lean

Modified src/algebra/order/smul.lean

Modified src/algebra/order/upper_lower.lean

Modified src/algebra/star/pointwise.lean

Modified src/data/finset/pointwise.lean

Modified src/data/set/pointwise/basic.lean

deleted theorem group.card_pow_eq_card_pow_card_univ

deleted theorem set.Inter_smul_subset

deleted theorem set.Inter_vsub_subset

deleted theorem set.Inter₂_smul_subset

deleted theorem set.Inter₂_vsub_subset

deleted theorem set.Union_inv_smul

deleted theorem set.Union_smul

deleted theorem set.Union_smul_eq_set_of_exists

deleted theorem set.Union_smul_left_image

deleted theorem set.Union_smul_right_image

deleted theorem set.Union_vsub

deleted theorem set.Union_vsub_left_image

deleted theorem set.Union_vsub_right_image

deleted theorem set.Union₂_smul

deleted theorem set.Union₂_vsub

deleted theorem set.bUnion_op_smul_set

deleted theorem set.bUnion_smul_set

deleted theorem set.empty_smul

deleted theorem set.empty_vsub

deleted theorem set.finite.inv

deleted theorem set.finite.mul

deleted theorem set.finite.smul

deleted theorem set.finite.smul_set

deleted theorem set.finite.vsub

deleted def set.fintype_mul

deleted theorem set.image2_smul

deleted theorem set.image2_vsub

deleted theorem set.image_smul

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_inv_smul_set_iff

deleted theorem set.mem_inv_smul_set_iff₀

deleted theorem set.mem_smul

deleted theorem set.mem_smul_set

deleted theorem set.mem_smul_set_iff_inv_smul_mem

deleted theorem set.mem_smul_set_iff_inv_smul_mem₀

deleted theorem set.mem_vsub

deleted theorem set.neg_smul_set

deleted theorem set.nonempty.of_smul_left

deleted theorem set.nonempty.of_smul_right

deleted theorem set.nonempty.of_vsub_left

deleted theorem set.nonempty.of_vsub_right

deleted theorem set.nonempty.smul

deleted theorem set.nonempty.smul_set

deleted theorem set.nonempty.smul_zero

deleted theorem set.nonempty.vsub

deleted theorem set.nonempty.zero_smul

deleted theorem set.op_smul_inter_ne_empty_iff

deleted theorem set.pairwise_disjoint_smul_iff

deleted theorem set.preimage_smul

deleted theorem set.preimage_smul_inv

deleted theorem set.preimage_smul_inv₀

deleted theorem set.preimage_smul₀

deleted theorem set.range_smul_range

deleted theorem set.set_smul_subset_iff

deleted theorem set.set_smul_subset_iff₀

deleted theorem set.set_smul_subset_set_smul_iff

deleted theorem set.set_smul_subset_set_smul_iff₀

deleted theorem set.singleton_smul

deleted theorem set.singleton_smul_singleton

deleted theorem set.singleton_vsub

deleted theorem set.singleton_vsub_singleton

deleted theorem set.smul_Inter_subset

deleted theorem set.smul_Inter₂_subset

deleted theorem set.smul_Union

deleted theorem set.smul_Union₂

deleted theorem set.smul_empty

deleted theorem set.smul_eq_empty

deleted theorem set.smul_inter_ne_empty_iff'

deleted theorem set.smul_inter_ne_empty_iff

deleted theorem set.smul_inter_subset

deleted theorem set.smul_mem_smul

deleted theorem set.smul_mem_smul_set

deleted theorem set.smul_mem_smul_set_iff

deleted theorem set.smul_mem_smul_set_iff₀

deleted theorem set.smul_nonempty

deleted theorem set.smul_set_Inter_subset

deleted theorem set.smul_set_Inter₂_subset

deleted theorem set.smul_set_Union

deleted theorem set.smul_set_Union₂

deleted theorem set.smul_set_empty

deleted theorem set.smul_set_eq_empty

deleted theorem set.smul_set_inter

deleted theorem set.smul_set_inter_subset

deleted theorem set.smul_set_inter₀

deleted theorem set.smul_set_mono

deleted theorem set.smul_set_neg

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_union

deleted theorem set.smul_set_univ

deleted theorem set.smul_set_univ₀

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_subset_smul_right

deleted theorem set.smul_union

deleted theorem set.smul_univ

deleted theorem set.smul_univ₀

deleted theorem set.smul_zero_subset

deleted theorem set.subset_set_smul_iff

deleted theorem set.subset_set_smul_iff₀

deleted theorem set.subsingleton_zero_smul_set

deleted theorem set.union_smul

deleted theorem set.union_vsub

deleted theorem set.vsub_Inter_subset

deleted theorem set.vsub_Inter₂_subset

deleted theorem set.vsub_Union

deleted theorem set.vsub_Union₂

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_subset_vsub_right

deleted theorem set.vsub_union

deleted theorem set.zero_mem_smul_iff

deleted theorem set.zero_mem_smul_set

deleted theorem set.zero_mem_smul_set_iff

deleted theorem set.zero_smul_set

deleted theorem set.zero_smul_set_subset

deleted theorem set.zero_smul_subset

Created src/data/set/pointwise/finite.lean

added theorem group.card_pow_eq_card_pow_card_univ

added theorem set.finite.inv

added theorem set.finite.mul

added theorem set.finite.smul

added theorem set.finite.smul_set

added theorem set.finite.vsub

added def set.fintype_mul

Created src/data/set/pointwise/smul.lean

added theorem set.Inter_smul_subset

added theorem set.Inter_vsub_subset

added theorem set.Inter₂_smul_subset

added theorem set.Inter₂_vsub_subset

added theorem set.Union_inv_smul

added theorem set.Union_smul

added theorem set.Union_smul_eq_set_of_exists

added theorem set.Union_smul_left_image

added theorem set.Union_smul_right_image

added theorem set.Union_vsub

added theorem set.Union_vsub_left_image

added theorem set.Union_vsub_right_image

added theorem set.Union₂_smul

added theorem set.Union₂_vsub

added theorem set.bUnion_op_smul_set

added theorem set.bUnion_smul_set

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_prod

added theorem set.image_vsub_prod

added theorem set.inter_smul_subset

added theorem set.inter_vsub_subset

added theorem set.mem_inv_smul_set_iff

added theorem set.mem_inv_smul_set_iff₀

added theorem set.mem_smul

added theorem set.mem_smul_set

added theorem set.mem_smul_set_iff_inv_smul_mem

added theorem set.mem_smul_set_iff_inv_smul_mem₀

added theorem set.mem_vsub

added theorem set.neg_smul_set

added theorem set.nonempty.of_smul_left

added theorem set.nonempty.of_smul_right

added theorem set.nonempty.of_vsub_left

added theorem set.nonempty.of_vsub_right

added theorem set.nonempty.smul

added theorem set.nonempty.smul_set

added theorem set.nonempty.smul_zero

added theorem set.nonempty.vsub

added theorem set.nonempty.zero_smul

added theorem set.op_smul_inter_ne_empty_iff

added theorem set.pairwise_disjoint_smul_iff

added theorem set.preimage_smul

added theorem set.preimage_smul_inv

added theorem set.preimage_smul_inv₀

added theorem set.preimage_smul₀

added theorem set.range_smul_range

added theorem set.set_smul_subset_iff

added theorem set.set_smul_subset_iff₀

added theorem set.set_smul_subset_set_smul_iff

added theorem set.set_smul_subset_set_smul_iff₀

added theorem set.singleton_smul

added theorem set.singleton_smul_singleton

added theorem set.singleton_vsub

added theorem set.singleton_vsub_singleton

added theorem set.smul_Inter_subset

added theorem set.smul_Inter₂_subset

added theorem set.smul_Union

added theorem set.smul_Union₂

added theorem set.smul_empty

added theorem set.smul_eq_empty

added theorem set.smul_inter_ne_empty_iff'

added theorem set.smul_inter_ne_empty_iff

added theorem set.smul_inter_subset

added theorem set.smul_mem_smul

added theorem set.smul_mem_smul_set

added theorem set.smul_mem_smul_set_iff

added theorem set.smul_mem_smul_set_iff₀

added theorem set.smul_nonempty

added theorem set.smul_set_Inter_subset

added theorem set.smul_set_Inter₂_subset

added theorem set.smul_set_Union

added theorem set.smul_set_Union₂

added theorem set.smul_set_empty

added theorem set.smul_set_eq_empty

added theorem set.smul_set_inter

added theorem set.smul_set_inter_subset

added theorem set.smul_set_inter₀

added theorem set.smul_set_mono

added theorem set.smul_set_neg

added theorem set.smul_set_nonempty

added theorem set.smul_set_range

added theorem set.smul_set_singleton

added theorem set.smul_set_subset_iff

added theorem set.smul_set_union

added theorem set.smul_set_univ

added theorem set.smul_set_univ₀

added theorem set.smul_singleton

added theorem set.smul_subset_iff

added theorem set.smul_subset_smul

added theorem set.smul_subset_smul_left

added theorem set.smul_subset_smul_right

added theorem set.smul_union

added theorem set.smul_univ

added theorem set.smul_univ₀

added theorem set.smul_zero_subset

added theorem set.subset_set_smul_iff

added theorem set.subset_set_smul_iff₀

added theorem set.subsingleton_zero_smul_set

added theorem set.union_smul

added theorem set.union_vsub

added theorem set.vsub_Inter_subset

added theorem set.vsub_Inter₂_subset

added theorem set.vsub_Union

added theorem set.vsub_Union₂

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_subset_vsub_left

added theorem set.vsub_subset_vsub_right

added theorem set.vsub_union

added theorem set.zero_mem_smul_iff

added theorem set.zero_mem_smul_set

added theorem set.zero_mem_smul_set_iff

added theorem set.zero_smul_set

added theorem set.zero_smul_set_subset

added theorem set.zero_smul_subset

Modified src/data/set/pointwise/support.lean

Modified src/data/set/semiring.lean

Modified src/group_theory/finiteness.lean

Modified src/group_theory/free_product.lean

Modified src/group_theory/group_action/basic.lean

Modified src/group_theory/submonoid/pointwise.lean

Modified src/order/filter/pointwise.lean