Linear lower bound on the growth of a generating set #
This file proves that the growth of a set generating an infinite group is at least linear.
theorem
Finset.pow_ssubset_pow_succ_of_pow_ne_closure
{G : Type u_1}
[Group G]
[DecidableEq G]
{X : Finset G}
{n : ℕ}
(hX₁ : 1 ∈ X)
(hX : X.Nontrivial)
(hXclosure : ↑X ^ n ≠ ↑(Subgroup.closure ↑X))
:
X ^ n ⊂ X ^ (n + 1)
theorem
Finset.nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{X : Finset G}
{n : ℕ}
(hX₁ : 0 ∈ X)
(hX : X.Nontrivial)
(hXclosure : n • ↑X ≠ ↑(AddSubgroup.closure ↑X))
:
n • X ⊂ (n + 1) • X
theorem
Finset.pow_right_strictMonoOn
{G : Type u_1}
[Group G]
[DecidableEq G]
{X : Finset G}
(hX₁ : 1 ∈ X)
(hX : X.Nontrivial)
:
StrictMonoOn (fun (n : ℕ) => X ^ n) {n : ℕ | ↑X ^ (n - 1) ≠ ↑(Subgroup.closure ↑X)}
theorem
Finset.nsmul_right_strictMonoOn
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{X : Finset G}
(hX₁ : 0 ∈ X)
(hX : X.Nontrivial)
:
StrictMonoOn (fun (n : ℕ) => n • X) {n : ℕ | (n - 1) • ↑X ≠ ↑(AddSubgroup.closure ↑X)}
theorem
Finset.pow_right_strictMono
{G : Type u_1}
[Group G]
[DecidableEq G]
{X : Finset G}
(hX₁ : 1 ∈ X)
(hXclosure : (↑(Subgroup.closure ↑X)).Infinite)
:
StrictMono fun (n : ℕ) => X ^ n
theorem
Finset.nsmul_right_strictMono
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{X : Finset G}
(hX₁ : 0 ∈ X)
(hXclosure : (↑(AddSubgroup.closure ↑X)).Infinite)
:
StrictMono fun (n : ℕ) => n • X
theorem
Finset.add_one_le_card_pow
{G : Type u_1}
[Group G]
[DecidableEq G]
{X : Finset G}
(hX₁ : 1 ∈ X)
(hXclosure : (↑(Subgroup.closure ↑X)).Infinite)
(n : ℕ)
:
The growth of a set generating an infinite group is at least linear.
theorem
Finset.add_nonneg_card_nsmul
{G : Type u_1}
[AddGroup G]
[DecidableEq G]
{X : Finset G}
(hX₁ : 0 ∈ X)
(hXclosure : (↑(AddSubgroup.closure ↑X)).Infinite)
(n : ℕ)
:
The growth of a set generating an infinite group is at least linear.