Chou.not_hasExponentialGrowth_of_isExponentiallyBounded
ProvedA finitely generated group which is exponentially bounded does not have exponential growth.
Preamble
import Definitions.Def_Chou_Growth import Mathlib
Formal statement
namespace Chou
theorem not_hasExponentialGrowth_of_isExponentiallyBounded {G : Type*} [Group G] [Group.FG G] (h : IsExponentiallyBounded G) : ¬ HasExponentialGrowth G := by sorry
end Chou