Theorem Finset.pairwiseDisjoint_smul_iff₀

Modification history

2026-04-27 14:17
Mathlib/Algebra/GroupWithZero/Action/Pointwise/Finset.lean
feat(Group/Action/Pointwise): generalise pairwiseDisjoint_smul to SMul rather than Mul (#38490) …
Added Finset.pairwiseDisjoint_smul_iff₀View on Github →