Commit 2026-04-27 14:17 94493509

View on Github →

feat(Group/Action/Pointwise): generalise pairwiseDisjoint_smul to SMul rather than Mul (#38490) and also add a group-with-zero version.

Estimated changes

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

modified theorem Finset.pairwiseDisjoint_smul_iff

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

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

added theorem Finset.pairwiseDisjoint_smul_iff₀