Commit 2026-09-16 23:41 7ef65c0f

View on Github →

feat(Pointwise/Finset): generalise smul_finset lemmas (#43455) Generalises card_smul_finset, smul_finset_inter, smul_finset_sdiff, smul_finset_symmDiff and smul_finset_subset_smul_finset_iff from group actions to IsLeftCancelSMul, and adds IsSMulRegular versions for a single regular element.

Estimated changes

Modified Mathlib/Algebra/Group/Action/Pointwise/Finset.lean

modified theorem Finset.mul_mem_smul_finset_iff

modified theorem Finset.smul_mem_smul_finset_iff

added theorem IsSMulRegular.card_smul_finset

added theorem IsSMulRegular.finset

added theorem IsSMulRegular.smul_finset_inter

added theorem IsSMulRegular.smul_finset_sdiff

added theorem IsSMulRegular.smul_finset_subset_smul_finset_iff

added theorem IsSMulRegular.smul_finset_symmDiff

Modified Mathlib/Algebra/Group/Action/Pointwise/Set/Basic.lean

added theorem IsSMulRegular.set

added theorem IsSMulRegular.smul_set_inter

added theorem IsSMulRegular.smul_set_sdiff

added theorem IsSMulRegular.smul_set_subset_smul_set_iff

added theorem IsSMulRegular.smul_set_symmDiff

modified theorem Set.smul_set_subset_smul_set_iff