Commit 2025-03-04 14:42 a9e8781d

View on Github →

chore: split off the action part of pointwise files (#22333) Move the parts of *.Pointwise.* that depend on MulAction to *.Action.Pointwise.* For the new copyright headers, see

Estimated changes

added theorem Finset.mul_singleton
added theorem Finset.singleton_mul
added theorem Finset.smul_univ
added theorem Fintype.piFinset_smul
added theorem Set.finite_smul_set
added theorem Set.infinite_smul_set
deleted theorem Finset.card_smul_finset
deleted theorem Finset.dens_smul_finset
deleted theorem Finset.image_smul_distrib
deleted theorem Finset.inv_smul_mem_iff
deleted theorem Finset.mul_singleton
deleted theorem Finset.singleton_mul
deleted theorem Finset.smul_finset_inter
deleted theorem Finset.smul_finset_sdiff
deleted theorem Finset.smul_finset_univ
deleted theorem Finset.smul_univ
deleted theorem Fintype.piFinset_smul
deleted theorem Set.finite_smul_set
deleted theorem Set.infinite_smul_set
added theorem Finset.smul_finset_neg
added theorem Finset.smul_univ₀'
added theorem Finset.smul_univ₀
added theorem Units.smul_mk0
deleted theorem Finset.Nonempty.smul_zero
deleted theorem Finset.Nonempty.zero_smul
deleted theorem Finset.smul_finset_neg
deleted theorem Finset.smul_univ₀'
deleted theorem Finset.smul_univ₀
deleted theorem Finset.smul_zero_subset
deleted theorem Finset.zero_mem_smul_iff
deleted theorem Finset.zero_smul_finset
deleted theorem Finset.zero_smul_subset
deleted theorem Units.smul_mk0
added theorem Finset.neg_smul_finset
deleted theorem Finset.neg_smul_finset