Theorem Finset.card_mul_finset_lt_two

Modification history

2025-10-25 23:37
Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
feat(Combinatorics/Additive/VerySmallDoubling): Hamidoune's Freiman-Kneser theorem for nonabelian groups (#28296) …
Added Finset.card_mul_finset_lt_twoView on Github →