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 : ℕ) : n + 1 ≤ (X ^ n).card

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 : ℕ) : n + 1 ≤ (n • X).card

The growth of a set generating an infinite group is at least linear.