dehn_function_groups
Provedalgebraanalysis
Dehn function of groups: The Dehn function δ_G(n) measures the difficulty of the word problem. Characterizing which functions arise as Dehn functions and the exact Dehn functions of specific groups remain active research.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem dehn_function_groups (G : Type*) [Group G]
(pres : List (FreeGroup (Fin 2)) × List (FreeGroup (Fin 2)))
(area : ℕ → ℕ) :
∃ (f : ℕ → ℕ), f = area := by
sorrySource