ZMod.min_le_card_add
theorem ZMod.min_le_card_add :
∀ {p : ℕ},
p.Prime → ∀ {s t : Finset (ZMod p)}, s.Nonempty → t.Nonempty → min p (s.card + t.card - 1) ≤ (s + t).card
The Cauchy-Davenport Theorem states that for any prime number `p`, and any two non-empty sets `s` and `t` in the integers modulo `p` (denoted as ℤ/pℤ), the size of the set that is the sum of `s` and `t` is at least `|s| + |t| - 1`, where `|s|` and `|t|` are the sizes of `s` and `t`, respectively, unless this quantity is greater than `p`. In the latter case, the minimum between `p` and the sum `|s| + |t| - 1` is taken.
More concisely: For any prime number $p$ and non-empty sets $s,t \subseteq \mathbb{Z}/p\mathbb{Z}$, the size of $s + t$ (the set of sums of elements from $s$ and $t$) satisfies $|s + t| \geq |s| + |t| - 1$, with $|s|$ and $|t|$ denoting their sizes, unless $|s| + |t| - 1 > p$, in which case $|s + t| \geq p$.
|
Finset.card_add_card_sub_one_le_card_mul
theorem Finset.card_add_card_sub_one_le_card_mul :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Semigroup α] [inst_2 : IsCancelMul α]
[inst_3 : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1] {s t : Finset α},
s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s * t).card
This is the **Cauchy-Davenport Theorem** for linearly ordered cancellative semigroups. The theorem states that for any type `α` that is a linearly ordered, cancellative semigroup (i.e., has operations that satisfy the properties of a semigroup, and those operations are cancellative, meaning `a * b = a * c` implies `b = c`), and has two covariant classes (i.e., if `x ≤ y` then `f x ≤ f y` for two specific multiplication functions), given two nonempty finite sets `s` and `t` of type `α`, the cardinality of the set `s` plus the cardinality of the set `t` minus one is less than or equal to the cardinality of the set `s * t` (i.e., the set obtained by multiplying every element of `s` with every element of `t`).
More concisely: For any linearly ordered, cancellative semigroup `α` with two covariant multiplication functions, the cardinality of the product of two finite, nonempty sets is greater than or equal to the sum of their cardinalities minus one.
|
Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mul
theorem Monoid.IsTorsionFree.card_add_card_sub_one_le_card_mul :
∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
Monoid.IsTorsionFree α → s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s * t).card
The Cauchy-Davenport Theorem for torsion-free groups states that for any type `α` that forms a group with decidable equality, and for any two nonempty finite sets `s` and `t` of this type `α`, if `α` forms a torsion-free monoid, then the sum of the sizes of `s` and `t` minus one is less than or equal to the size of the product set `s * t`. This means that in a torsion-free group, the size of the set formed by multiplying all possible pairs from two nonempty sets is at least as large as the sum of the sizes of the original sets, minus one.
More concisely: In a torsion-free group, the size of the product of two nonempty finite sets is greater than or equal to the sum of their sizes minus one.
|
Finset.min_le_card_add
theorem Finset.min_le_card_add :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
s.Nonempty → t.Nonempty → min (AddMonoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s + t).card
This theorem is a generalization of the Cauchy-Davenport theorem to arbitrary groups. It states that for any type `α` that has an additive group structure and decidable equality, and for any two nonempty finite sets `s` and `t` of `α`, the minimum of the smallest subgroup order and the sum of the sizes of `s` and `t` minus one, is less than or equal to the size of the set `s + t`, which is the set of all elements that can be obtained by adding an element of `s` to an element of `t`. In other words, the size of `s + t` is at least as large as `|s| + |t| - 1`, unless this quantity is greater than the order of the smallest nontrivial subgroup.
More concisely: For any finite additive group `α` with decidable equality and any two finite nonempty subsets `s` and `t` of `α`, the size of `s + t` is bounded above by the minimum of the sum of their sizes and the order of the smallest nontrivial subgroup.
|
AddMonoid.IsTorsionFree.card_add_card_sub_nonneg_card_add
theorem AddMonoid.IsTorsionFree.card_add_card_sub_nonneg_card_add :
∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : DecidableEq α] {s t : Finset α},
AddMonoid.IsTorsionFree α → s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s + t).card
The **Cauchy-Davenport theorem** for torsion-free groups is stated as follows: Given any type `α` which is an additive group where equality is decidable, and any two finite sets `s` and `t` of this type, if `α` satisfies the property that it is torsion-free (i.e., only the element 0 has finite order), and both `s` and `t` are nonempty, then the size of the set resulting from adding each element of `s` to each element of `t` is at least the sum of the sizes of `s` and `t` minus 1. This theorem provides a lower bound on the size of the resulting set from the addition operation.
More concisely: In a torsion-free additive group where equality is decidable, the size of the set of sums of every element from two nonempty finite sets is at least the sum of their sizes minus 1.
|
Finset.min_le_card_mul
theorem Finset.min_le_card_mul :
∀ {α : Type u_1} [inst : Group α] [inst_1 : DecidableEq α] {s t : Finset α},
s.Nonempty → t.Nonempty → min (Monoid.minOrder α) ↑(s.card + t.card - 1) ≤ ↑(s * t).card
This theorem is a generalization of the Cauchy-Davenport theorem to arbitrary groups. It states that for any type `α` that forms a group (with decidable equality), given two non-empty finite sets `s` and `t` of type `α`, the minimum of the minimal order of the group `α` and the quantity `|s| + |t| - 1` (where `|s|` and `|t|` represents the cardinalities of `s` and `t` respectively), is less than or equal to the cardinality of the set formed by multiplying all elements of `s` and `t` together. In other words, the size of the resulting set `s * t` is at least `|s| + |t| - 1`, unless this quantity is greater than the size of the smallest non-trivial subgroup of the group.
More concisely: The cardinality of the product of two non-empty finite sets in a group with decidable equality is at least their sum minus one, up to the size of the smallest non-trivial subgroup.
|
Finset.card_add_card_sub_nonneg_card_add
theorem Finset.card_add_card_sub_nonneg_card_add :
∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddSemigroup α] [inst_2 : IsCancelAdd α]
[inst_3 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1]
[inst_4 : CovariantClass α α (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] {s t : Finset α},
s.Nonempty → t.Nonempty → s.card + t.card - 1 ≤ (s + t).card
The **Cauchy-Davenport theorem** for linearly ordered additive cancellative semigroups states that for any two nonempty finite sets `s` and `t` of a type `α`, where `α` is a linearly ordered additive cancellative semigroup satisfying certain covariance properties, the size of the set obtained by adding every element of `s` to every element of `t` is at least the sum of the sizes of `s` and `t` minus 1. In mathematical notation, this is expressed as `|s| + |t| - 1 ≤ |s + t|`.
More concisely: In a linearly ordered, additive cancellative semigroup `α` with covariance properties, the size of the set of sums of an element from any two finite nonempty sets `s` and `t` is at least the sum of their sizes minus one. (i.e., `|s + t| ≥ |s| + |t| - 1`)
|
Mathlib.Combinatorics.SetFamily.CauchyDavenport._auxLemma.8
theorem Mathlib.Combinatorics.SetFamily.CauchyDavenport._auxLemma.8 :
∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α]
[inst_2 : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1] [inst_3 : ZeroLEOneClass α]
[inst_4 : CharZero α] {m n : ℕ}, (↑m ≤ ↑n) = (m ≤ n)
The theorem states that for any type `α` which is an additive monoid with one, a partial order, has a covariance class defined for addition and less than or equal to relation, has zero less than or equal to one, and character zero, the inequality between two natural numbers `m` and `n` holds if and only if the inequality between their corresponding elements in `α` holds. This means that the ordering of `m` and `n` as natural numbers is preserved when they are viewed as elements of the type `α`.
More concisely: For any additive monoid with one, partially ordered type `α` with zero less than one and character zero, the order relation between natural numbers corresponds to the order relation between their corresponding elements in `α`.
|