Theorems · Theorem · group theory

AddCommGroup.fg_of_descent

∀ {G : Type u_1} [inst : AddCommGroup G] {n : ℕ} {h : G → ℝ} {a b c₀ : ℝ} {c : G → ℝ},
  0 ≤ a →
    a < b →
      (nsmulAddMonoidHom n).range.FiniteIndex →
        (∀ (g x : G), h x ≤ a * h (g + x) + c g) →
          (∀ (x : G), b * h x - c₀ ≤ h (n • x)) → ∀ [Northcott h], AddGroup.FG G

If G is a commutative additive group and n : ℕ, h : G → ℝ satisfy * G / n • G is finite, * for all g x : G, h x ≤ a * h (g + x) + c g, * for all x : G, h (n • x) ≥ b * h x - c₀, * for all B : ℝ, there are only finitely many x : G such that h x ≤ B, where 0 ≤ a < b and c₀ are real numbers, c : G → ℝ, then G is finitely generated.

Defined in

Mathlib.GroupTheory.Descent

Cited by

1 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupNorthcott