Commit 2024-11-28 20:24 4e9fa40d

View on Github →

feat: s ⊆ s ^ n when 1 ∈ s (#19538) and the product of nontrivial sets is nontrivial. From GrowthInGroups

Estimated changes

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

added theorem Finset.Nontrivial.mul

added theorem Finset.Nontrivial.mul_left

added theorem Finset.Nontrivial.mul_right

added theorem Finset.Nontrivial.pow

modified theorem Finset.card_le_card_mul_right

modified theorem Finset.card_le_card_mul_self'

modified theorem Finset.card_mul_singleton

modified theorem Finset.card_singleton_mul

modified theorem Finset.inter_mul_singleton

modified theorem Finset.singleton_mul_inter

added theorem Finset.subset_pow

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

added theorem Set.Nontrivial.mul

added theorem Set.Nontrivial.mul_left

added theorem Set.Nontrivial.mul_right

added theorem Set.Nontrivial.pow

added theorem Set.subset_pow

Modified Mathlib/Combinatorics/Additive/CauchyDavenport.lean

Modified Mathlib/Combinatorics/Additive/PluenneckeRuzsa.lean