Theorems · Theorem · group theory

Group.fg_of_descent

∀ {G : Type u_1} [inst : Group G] {f : G →* G},
  (∀ (U : Subgroup G), Subgroup.map f U ≤ U) →
    ∀ {s : Set G} {h : G → ℝ} {a b c : ℝ},
      0 ≤ a →
        a < b →
          s.Finite →
            s * ↑f.range = Set.univ →
              (∀ g ∈ s, ∀ (x : G), h x ≤ a * h (g * x) + c) →
                (∀ (x : G), b * h x - c ≤ h (f x)) → ∀ [Northcott h], Group.FG G

If G is a group and f : G →* G is an endomorphism sending subgroups into themselves, and if there is a "height function" h : G → ℝ with respect to f and a finite subset s of G, then G is finitely generated.

Defined in

Mathlib.GroupTheory.Descent

Cited by

1 results in Mathlib

Foundations

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

Assumes

GroupNorthcott