Theorem Finset.mul_mem_smul_finset_iff

Modification history

2026-09-16 23:41
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
feat(Pointwise/Finset): generalise smul_finset lemmas (#43455) …
Modified Finset.mul_mem_smul_finset_iffView on Github →
2025-10-09 10:11
Mathlib/Algebra/Group/Action/Pointwise/Finset.lean
feat(Combinatorics/Additive/VerySmallDoubling): weak non-commutative Kneser's theorem (#26660) …
Added Finset.mul_mem_smul_finset_iffView on Github →