Theorems · Theorem · group theory

Monoid.finite_set_isOfFiniteOrder_of_descent

∀ {M : Type u_1} [inst : Monoid M] {n : ℕ} {h : M → ℝ} {b c₀ : ℝ},
  1 < b → (∀ (x : M), b * h x - c₀ ≤ h (x ^ n)) → ∀ [Northcott h], Finite ↑{x | IsOfFinOrder x}

If M is a monoid and n : ℕ, h : M → ℝ satisfy * for all M : G, h (x ^ n) ≥ b * h x - c₀, * for all B : ℝ, there are only finitely many x : M such that h x ≤ B, where 1 < b and c₀ are real numbers, then the set of elements of finite order in M is finite.

Defined in

Mathlib.GroupTheory.Descent

Cited by

1 results in Mathlib

Foundations

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

Assumes

MonoidNorthcott